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  5297  funopab  5303  funco  5308  funcnv2  5328  funcnv  5329  fun2cnv  5332  fncnv  5334  imadif  5348  fnres  5386  ovi3  6073  oprabex3  6204  axaddf  7963  axmulf  7964  frecuzrdgtcl  10538  frecuzrdgfunlem  10545  fsum3  11617