Theorem mobii 2630

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 2628	. 2 ⊢ (⊤ → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
4	3	trud 1642	1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Syntax hints:   ↔ wb 196  ⊤wtru 1633  ∃*wmo 2608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-12 2196

This theorem depends on definitions:  df-bi 197  df-tru 1635  df-ex 1854  df-nf 1859  df-eu 2611  df-mo 2612

This theorem is referenced by:  moanmo  2670  2moswap  2685  rmobiia  3271  rmov  3362  euxfr2  3532  rmoan  3547  2reu5lem2  3555  reuxfr2d  5040  dffun9  6078  funopab  6084  funcnv2  6118  funcnv  6119  fun2cnv  6121  fncnv  6123  imadif  6134  fnres  6168  ov3  6963  oprabex3  7323  brdom6disj  9566  grothprim  9868  axaddf  10178  axmulf  10179  reuxfr3d  29658  funcnvmptOLD  29797  funcnvmpt  29798  alrmomorn  34464  cosscnvssid4  34568  2rmoswap  41708