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 1407	1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Syntax hints:   ↔ wb 105  ⊤wtru 1399  ∃*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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

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

This theorem is referenced by:  moaneu  2156  moanmo  2157  2moswapdc  2170  2exeu  2172  rmobiia  2725  rmov  2824  euxfr2dc  2992  rmoan  3007  2rmorex  3013  mosn  3709  dffun9  5362  funopab  5368  funco  5373  funcnv2  5397  funcnv  5398  fun2cnv  5401  fncnv  5403  imadif  5417  fnres  5456  ovi3  6169  oprabex3  6300  axaddf  8131  axmulf  8132  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  fsum3  12011