Theorem mobii 2092

Description: Formula-building rule for "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		mobii.1	. . . 4 ⊢ (𝜓 ↔ 𝜒)
2	1	a1i 9	. . 3 ⊢ (⊤ → (𝜓 ↔ 𝜒))
3	2	mobidv 2091	. 2 ⊢ (⊤ → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
4	3	mptru 1382	1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Syntax hints:   ↔ wb 105  ⊤wtru 1374  ∃*wmo 2056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-eu 2058  df-mo 2059

This theorem is referenced by:  moaneu  2131  moanmo  2132  2moswapdc  2145  2exeu  2147  rmobiia  2697  rmov  2794  euxfr2dc  2962  rmoan  2977  2rmorex  2983  mosn  3674  dffun9  5309  funopab  5315  funco  5320  funcnv2  5343  funcnv  5344  fun2cnv  5347  fncnv  5349  imadif  5363  fnres  5402  ovi3  6096  oprabex3  6227  axaddf  8001  axmulf  8002  frecuzrdgtcl  10579  frecuzrdgfunlem  10586  fsum3  11773