Theorem mobii 1398

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 1122	. 2 |- x = x
2		hbequid 1165	. . 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 1397	. 2 |- (x = x -> (E*xps <-> E*xch))
6	1, 5	ax-mp 7	1 |- (E*xps <-> E*xch)

Syntax hints:   <-> wb 146  E*wmo 1374

This theorem is referenced by:  mooran1 1418  mooran2 1419  moaneu 1423  moanmo 1424  euor2 1430  2moswap 1437  2exeu 1439  2eu1 1442  euxfr2 1916  reuxfr2 2893  dffun8 3527  funopab 3534  funco 3536  funcnv2 3542  funcnv 3543  fun2cnv 3545  fncnv 3547  funin 3552  imadif 3560  fconst 3643  f11 3649  oprabex3 4007  oprabval3 4015  brdom7disj 4776  brdom6disj 4777  axaddopr 5237  axmulopr 5238  spwmo 8580  grothprim 8722  bra11 9954

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-eu 1375  df-mo 1376

Copyright terms: Public domain