Theorem mobii 2090

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

Syntax hints:   ↔ wb 105  ⊤wtru 1373  ∃*wmo 2054

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-eu 2056  df-mo 2057

This theorem is referenced by:  moaneu  2129  moanmo  2130  2moswapdc  2143  2exeu  2145  rmobiia  2695  rmov  2791  euxfr2dc  2957  rmoan  2972  2rmorex  2978  mosn  3668  dffun9  5299  funopab  5305  funco  5310  funcnv2  5333  funcnv  5334  fun2cnv  5337  fncnv  5339  imadif  5353  fnres  5391  ovi3  6082  oprabex3  6213  axaddf  7980  axmulf  7981  frecuzrdgtcl  10555  frecuzrdgfunlem  10562  fsum3  11640