Theorem mobii 1934

Description: Formula-building rule for "at most one" quantifier (inference rule). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.)

Hypothesis

Ref	Expression
mobii.1	⊢ (ψ ↔ χ)

Assertion

Ref	Expression
mobii	⊢ (∃*xψ ↔ ∃*xχ)

Proof of Theorem mobii

Step	Hyp	Ref	Expression
1		mobii.1	. . . 4 ⊢ (ψ ↔ χ)
2	1	a1i 9	. . 3 ⊢ ( ⊤ → (ψ ↔ χ))
3	2	mobidv 1933	. 2 ⊢ ( ⊤ → (∃*xψ ↔ ∃*xχ))
4	3	trud 1251	1 ⊢ (∃*xψ ↔ ∃*xχ)

Syntax hints:   ↔ wb 98   ⊤ wtru 1243  ∃*wmo 1898

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424

This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-eu 1900  df-mo 1901

This theorem is referenced by:  moaneu  1973  moanmo  1974  2moswapdc  1987  2exeu  1989  rmobiia  2493  rmov  2568  euxfr2dc  2720  rmoan  2733  2rmorex  2739  mosn  3398  dffun9  4873  funopab  4878  funco  4883  funcnv2  4902  funcnv  4903  fun2cnv  4906  fncnv  4908  imadif  4922  fnres  4958  ovi3  5579  oprabex3  5698  frecuzrdgfn  8879