Theorem mobii 1382

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

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

This theorem is referenced by:  mooran1 1402  mooran2 1403  moaneu 1407  moanmo 1408  euor2 1414  2moswap 1421  2exeu 1423  2eu1 1426  euxfr2 1897  reuxfr2 2866  dffun8 3482  funopab 3488  funco 3490  funcnv2 3496  funcnv 3497  fun2cnv 3499  fncnv 3501  funin 3506  imadif 3514  fconst 3597  f11 3603  oprabex3 3961  oprabval3 3969  brdom7disj 4728  brdom6disj 4729  axaddopr 5188  axmulopr 5189  grothprim 8635  bra11 10168

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-gen 955  ax-9 1102  ax-12 1104  ax-17 1190

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-eu 1359  df-mo 1360

Copyright terms: Public domain