Theorem mobii 2568

Description: Formula-building rule for the at-most-one quantifier (inference form). (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		mobi 2566	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
2		mobii.1	. 2 ⊢ (𝜓 ↔ 𝜒)
3	1, 2	mpg 1892	1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Syntax hints:   ↔ wb 197  ∃*wmo 2563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005

This theorem depends on definitions:  df-bi 198  df-ex 1875  df-mo 2565

This theorem is referenced by:  moanmo  2654  2moswap  2669  nulmo  2750  rmoanid  3068  rmobiia  3280  rmov  3375  euxfr2  3552  rmoan  3569  2reu5lem2  3577  reuxfr2d  5056  dffun9  6099  funopab  6105  funcnv2  6137  funcnv  6138  fun2cnv  6140  fncnv  6142  imadif  6153  fnres  6187  ov3  6997  oprabex3  7357  brdom6disj  9609  grothprim  9911  axaddf  10221  axmulf  10222  reuxfr3d  29786  funcnvmpt  29920  alrmomorn  34555  cosscnvssid4  34659  euabsneu  41813  2rmoswap  41858