Theorem mobii 2079

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

Syntax hints:   ↔ wb 105  ⊤wtru 1365  ∃*wmo 2043

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-eu 2045  df-mo 2046

This theorem is referenced by:  moaneu  2118  moanmo  2119  2moswapdc  2132  2exeu  2134  rmobiia  2684  rmov  2780  euxfr2dc  2945  rmoan  2960  2rmorex  2966  mosn  3654  dffun9  5283  funopab  5289  funco  5294  funcnv2  5314  funcnv  5315  fun2cnv  5318  fncnv  5320  imadif  5334  fnres  5370  ovi3  6055  oprabex3  6181  axaddf  7928  axmulf  7929  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  fsum3  11530