Theorem mobii 1444

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

Hypothesis

Ref	Expression
mobii.1	|- (ps <-> ch)

Assertion

Ref	Expression
mobii	|- (E*xps <-> E*xch)

Proof of Theorem mobii

Step	Hyp	Ref	Expression
1		equid 1162	. 2 |- x = x
2		hbequid 1206	. . 3 |- (x = x -> A.x x = x)
3		mobii.1	. . . 4 |- (ps <-> ch)
4	3	a1i 8	. . 3 |- (x = x -> (ps <-> ch))
5	2, 4	mobid 1443	. 2 |- (x = x -> (E*xps <-> E*xch))
6	1, 5	ax-mp 7	1 |- (E*xps <-> E*xch)

Syntax hints:   <-> wb 144  E*wmo 1420

This theorem is referenced by:  mooran1 1464  mooran2 1465  moaneu 1469  moanmo 1470  euor2 1477  2moswap 1484  2exeu 1486  2eu1 1489  euxfr2 1972  reuxfr2 3126  dffun9 3646  funopab 3653  funco 3655  funcnv2 3661  funcnv 3662  fun2cnv 3664  fncnv 3666  funin 3671  imadif 3679  fconst 3765  dff12 3771  oprabex3 4082  oprabval3 4090  brdom7disj 4950  brdom6disj 4951  axaddopr 5419  axmulopr 5420  spwmo 8918  grothprim 9057  bra11 10321

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-eu 1421  df-mo 1422

Copyright terms: Public domain