Theorem mobii 2641

Description: Formula-building rule for "at most one" quantifier (inference rule). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.)

Hypothesis

Ref	Expression
mobii.1	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
mobii	⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Proof of Theorem mobii

Step	Hyp	Ref	Expression
1		mobii.1	. . . 4 ⊢ (𝜓 ↔ 𝜒)
2	1	a1i 11	. . 3 ⊢ (⊤ → (𝜓 ↔ 𝜒))
3	2	mobidv 2639	. 2 ⊢ (⊤ → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
4	3	trud 1641	1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Syntax hints:   ↔ wb 196  ⊤wtru 1632  ∃*wmo 2619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203

This theorem depends on definitions:  df-bi 197  df-tru 1634  df-ex 1853  df-nf 1858  df-eu 2622  df-mo 2623

This theorem is referenced by:  moanmo  2681  2moswap  2696  rmobiia  3281  rmov  3374  euxfr2  3543  rmoan  3558  2reu5lem2  3566  reuxfr2d  5019  dffun9  6060  funopab  6066  funcnv2  6097  funcnv  6098  fun2cnv  6100  fncnv  6102  imadif  6113  fnres  6147  ov3  6944  oprabex3  7304  brdom6disj  9556  grothprim  9858  axaddf  10168  axmulf  10169  reuxfr3d  29668  funcnvmptOLD  29807  funcnvmpt  29808  alrmomorn  34465  cosscnvssid4  34569  2rmoswap  41704