Theorem ralrimiva 2697

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)

Hypothesis

Ref	Expression
ralrimiva.1	|- ((ph /\ x e. A) -> ps)

Assertion

Ref	Expression
ralrimiva	|- (ph -> A.x e. A ps)

Distinct variable group:   ph,x

Allowed substitution hints:   ps(x)   A(x)

Proof of Theorem ralrimiva

Step	Hyp	Ref	Expression
1		ralrimiva.1	. . 3 |- ((ph /\ x e. A) -> ps)
2	1	ex 423	. 2 |- (ph -> (x e. A -> ps))
3	2	ralrimiv 2696	1 |- (ph -> A.x e. A ps)

Syntax hints:   -> wi 4   /\ wa 358   e. wcel 1710  A.wral 2614

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2619

This theorem is referenced by:  ralrimivvva  2707  rgen2  2710  rgen3  2711  nrexdv  2717  rabbidva  2850  ssrabdv  3345  ss2rabdv  3347  rgenz  3655  iuneq2dv  3990  ssofss  4076  findsd  4410  evenodddisj  4516  tfinnn  4534  vfinspss  4551  vfinspclt  4552  fun11iun  5305  eqfnfvd  5395  dff3  5420  dffo4  5423  foco2  5426  ffnfv  5427  ffvresb  5431  fconst2g  5452  fconstfv  5456  fmptd  5694  f1od  5726  extd  5923  refrd  5926  enmap2lem5  6067  enmap1lem5  6073  spacis  6288  nchoicelem12  6300  nchoicelem17  6305