Theorem mobii 1801

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 1484	. 2 |- x = x
2		hbequid2 1533	. . 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 1800	. 2 |- (x = x -> (E*xps <-> E*xch))
6	1, 5	ax-mp 7	1 |- (E*xps <-> E*xch)

Syntax hints:   <-> wb 163  E*wmo 1772

This theorem is referenced by:  mooran1OLD 1823  mooran2OLD 1825  moaneu 1830  moanmo 1831  euor2OLD 1840  2moswap 1848  2exeu 1850  2eu1 1853  euxfr2 2437  reuxfr2d 3844  reuxfr2 3845  dffun9 4450  funopab 4455  funcoOLD 4458  funsn 4463  funcnv2 4474  funcnv 4475  fun2cnv 4477  fncnv 4479  funinOLD 4485  imadif 4493  fconstOLD 4603  dff12 4609  oprabex3 4951  oprabval3 4959  brdom7disj 5966  brdom6disj 5967  axaddopr 6417  axmulopr 6418  spwmo 9999  grothprim 10141  bra11 11679  bnj149 13241  isline1 15294

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-eu 1775  df-mo 1776

Copyright terms: Public domain