Theorem mobii 2492

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

Syntax hints:   ↔ wb 196  ⊤wtru 1481  ∃*wmo 2470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044

This theorem depends on definitions:  df-bi 197  df-tru 1483  df-ex 1702  df-nf 1707  df-eu 2473  df-mo 2474

This theorem is referenced by:  moanmo  2531  2moswap  2546  rmobiia  3125  rmov  3212  euxfr2  3378  rmoan  3393  2reu5lem2  3401  reuxfr2d  4861  dffun9  5886  funopab  5891  funcnv2  5925  funcnv  5926  fun2cnv  5928  fncnv  5930  imadif  5941  fnres  5975  ov3  6762  oprabex3  7117  brdom6disj  9314  grothprim  9616  axaddf  9926  axmulf  9927  reuxfr3d  29218  funcnvmptOLD  29351  funcnvmpt  29352  2rmoswap  40518