Theorem bimo 1031

Description: Formula-building rule for "at most one" quantifier (inference rule).

Hypothesis

Ref	Expression
bimo.1	⊢ (ψ ↔ χ)

Assertion

Ref	Expression
bimo	⊢ (∃*xψ ↔ ∃*xχ)

Proof of Theorem bimo

Step	Hyp	Ref	Expression
1		eqid 810	. 2 ⊢ x = x
2	1	hbth 697	. . 3 ⊢ (x = x → ∀x x = x)
3		bimo.1	. . . 4 ⊢ (ψ ↔ χ)
4	3	a1i 7	. . 3 ⊢ (x = x → (ψ ↔ χ))
5	2, 4	bimod 1030	. 2 ⊢ (x = x → (∃*xψ ↔ ∃*xχ))
6	1, 5	ax-mp 6	1 ⊢ (∃*xψ ↔ ∃*xχ)

Syntax hints:   ↔ wb 127   = weq 797  ∃*wmo 1008

This theorem is referenced by:  mooran1 1049  mooran2 1050  2moswap 1064  2exeu 1066  2eu1 1067  euxfr2 1435  reuxfr2 1579  funopab 2694  funco 2696  funcnv2 2702  funcnv 2703  fun2cnv 2704  funin 2708  imadif 2714  fconst 2774  f11 2780  oprabex3 3046  oprabval3 3052

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-9 799  ax-12 802  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-eu 1009  df-mo 1010

metamath.org