Theorem r19.21v 2178

Description: Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers. (The proof was shortened by Andrew Salmon, 30-May-2011.)

Assertion

Ref	Expression
r19.21v	|- (A.x e. A (ph -> ps) <-> (ph -> A.x e. A ps))

Distinct variable group:   ph,x

Proof of Theorem r19.21v

Step	Hyp	Ref	Expression
1		r19.21t 2177	. 2 |- (A.x(ph -> A.xph) -> (A.x e. A (ph -> ps) <-> (ph -> A.x e. A ps)))
2		ax-17 1317	. 2 |- (ph -> A.xph)
3	1, 2	mpg 1332	1 |- (A.x e. A (ph -> ps) <-> (ph -> A.x e. A ps))

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296  A.wral 2105

This theorem is referenced by:  r19.32v 2230  rcla4dv 2382  rmo4 2445  sbcralt 2527  sbcralgf 2529  ssiin 3302  ssiinOLD 3303  dftr5 3414  tfinds2 3947  tfinds3 3948  tfr3 5134  oeordi 5262  oaabs 5309  raluz2 7612  cau5i 8171  climaddlem3 8376  climmullem8 8387  metcn4 9249  bnj85 13212  bnj515 13256  ndvdssub 13710  gcdcllem1 13718  cnfillim 15590  flimfcn 15603  isfclus 15606  fcluscn 15619  fclsfcn 15632

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

This theorem depends on definitions:  df-bi 164  df-an 242  df-ral 2109

Copyright terms: Public domain