Theorem mobii 1404

Description: Formula-building rule for "at most one" quantifier (inference rule).

Hypothesis

Ref	Expression
mobii.1	⊢ (ψ ↔ χ)

Assertion

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

Proof of Theorem mobii

Step	Hyp	Ref	Expression
1		equid 1125	. 2 ⊢ x = x
2		hbequid 1168	. . 3 ⊢ (x = x → ∀x x = x)
3		mobii.1	. . . 4 ⊢ (ψ ↔ χ)
4	3	a1i 8	. . 3 ⊢ (x = x → (ψ ↔ χ))
5	2, 4	mobid 1403	. 2 ⊢ (x = x → (∃*xψ ↔ ∃*xχ))
6	1, 5	ax-mp 7	1 ⊢ (∃*xψ ↔ ∃*xχ)

Syntax hints:   ↔ wb 146  ∃*wmo 1380

This theorem is referenced by:  mooran1 1424  mooran2 1425  moaneu 1429  moanmo 1430  euor2 1436  2moswap 1443  2exeu 1445  2eu1 1448  euxfr2 1923  reuxfr2 2899  dffun8 3537  funopab 3544  funco 3546  funcnv2 3552  funcnv 3553  fun2cnv 3555  fncnv 3557  funin 3562  imadif 3570  fconst 3653  f11 3659  oprabex3 4017  oprabval3 4025  brdom7disj 4787  brdom6disj 4788  axaddopr 5248  axmulopr 5249  spwmo 8613  grothprim 8738  bra11 9997

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-eu 1381  df-mo 1382

Copyright terms: Public domain