Theorem mobii 1937

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

Proof of Theorem mobii

Step	Hyp	Ref	Expression
1		mobii.1	. . . 4 ⊢ (𝜓 ↔ 𝜒)
2	1	a1i 9	. . 3 ⊢ (⊤ → (𝜓 ↔ 𝜒))
3	2	mobidv 1936	. 2 ⊢ (⊤ → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
4	3	trud 1252	1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Syntax hints:   ↔ wb 98  ⊤wtru 1244  ∃*wmo 1901

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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-eu 1903  df-mo 1904

This theorem is referenced by:  moaneu  1976  moanmo  1977  2moswapdc  1990  2exeu  1992  rmobiia  2499  rmov  2574  euxfr2dc  2726  rmoan  2739  2rmorex  2745  mosn  3406  dffun9  4930  funopab  4935  funco  4940  funcnv2  4959  funcnv  4960  fun2cnv  4963  fncnv  4965  imadif  4979  fnres  5015  ovi3  5637  oprabex3  5756  frecuzrdgfn  9198