Theorem r19.21v 1719

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 973	. . 3 |- (ph -> A.xph)
2	1	ax-gen 965	. 2 |- A.x(ph -> A.xph)
3		r19.21t 1718	. 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 956  A.wral 1648

This theorem is referenced by:  r19.32v 1761  rcla4dv 1881  rmo4 1936  sbcralt 1993  sbcralgf 1995  ssiin 2603  dftr5 2688  tfinds2 3171  tfinds3 3172  tfr3 3932  oeordi 4220  oaabs 4258  raluz2 6444  cau5 6919  climaddlem3 7116  climmullem8 7127  metcn4 7968

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980

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

Copyright terms: Public domain