Theorem mobii 2116

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

Syntax hints:   ↔ wb 105  ⊤wtru 1398  ∃*wmo 2080

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-eu 2082  df-mo 2083

This theorem is referenced by:  moaneu  2156  moanmo  2157  2moswapdc  2170  2exeu  2172  rmobiia  2724  rmov  2823  euxfr2dc  2991  rmoan  3006  2rmorex  3012  mosn  3705  dffun9  5355  funopab  5361  funco  5366  funcnv2  5390  funcnv  5391  fun2cnv  5394  fncnv  5396  imadif  5410  fnres  5449  ovi3  6158  oprabex3  6290  axaddf  8087  axmulf  8088  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  fsum3  11947