Theorem mobii 2481

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 11	. . 3 ⊢ (⊤ → (𝜓 ↔ 𝜒))
3	2	mobidv 2479	. 2 ⊢ (⊤ → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
4	3	trud 1484	1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Syntax hints:   ↔ wb 195  ⊤wtru 1476  ∃*wmo 2459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-tru 1478  df-ex 1696  df-nf 1701  df-eu 2462  df-mo 2463

This theorem is referenced by:  moanmo  2520  2moswap  2535  rmobiia  3109  rmov  3195  euxfr2  3358  rmoan  3373  2reu5lem2  3381  reuxfr2d  4817  dffun9  5832  funopab  5837  funcnv2  5871  funcnv  5872  fun2cnv  5874  fncnv  5876  imadif  5887  fnres  5921  ov3  6695  oprabex3  7048  brdom6disj  9235  grothprim  9535  axaddf  9845  axmulf  9846  reuxfr3d  28713  funcnvmptOLD  28850  funcnvmpt  28851  2rmoswap  39833