Theorem r19.21v 1708

Description: Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers.

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		ax-17 968	. . 3 |- (ph -> A.xph)
2	1	ax-gen 960	. 2 |- A.x(ph -> A.xph)
3		r19.21t 1707	. 2 |- (A.x(ph -> A.xph) -> (A.x e. A (ph -> ps) <-> (ph -> A.x e. A ps)))
4	2, 3	ax-mp 7	1 |- (A.x e. A (ph -> ps) <-> (ph -> A.x e. A ps))

Syntax hints:   -> wi 3   <-> wb 146  A.wal 951  A.wral 1637

This theorem is referenced by:  r19.32v 1750  rcla4dv 1869  rmo4 1923  sbcralt 1980  sbcralgf 1982  ssiin 2589  dftr5 2673  tfinds2 3155  tfinds3 3156  tfr3 3911  oeordi 4198  oaabs 4236  raluz2 6375  cau5 6856  climaddlem3 7052  climmullem8 7063  metcn4 7905

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1641

Copyright terms: Public domain