Theorem ralrimiva 2386

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 108	. 2 |- (ph -> (x e. A -> ps))
3	2	ralrimiv 2385	1 |- (ph -> A.x e. A ps)

Syntax hints:   -> wi 4   /\ wa 97   e. wcel 1390  A.wral 2300

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305

This theorem is referenced by:  ralrimivvva  2396  rgen2  2399  rgen3  2400  nrexdv  2406  r19.29vva  2450  rabbidva  2542  ssrabdv  3013  ss2rabdv  3015  iuneq2dv  3669  disjeq2dv  3741  mpteq12dva  3829  triun  3858  issod  4047  peano2  4261  fun11iun  5090  fniinfv  5174  eqfnfv  5208  eqfnfvd  5211  dff3im  5255  dffo4  5258  foco2  5261  fmptd  5265  ffnfv  5266  fmpt2d  5270  ffvresb  5271  fconst2g  5319  fconstfvm  5322  resfunexg  5325  eufnfv  5332  fniunfv  5344  fcofo  5367  fliftel  5376  fliftfun  5379  fliftfuns  5381  riota5f  5435  grprinvlem  5637  grprinvd  5638  f1ocnvd  5644  suppssov1  5651  offval2  5668  ofrfval2  5669  offveqb  5672  caofref  5674  caofinvl  5675  opabex3d  5690  tfrlem1  5864  tfrlemisucaccv  5880  tfrlemiubacc  5885  omcl  5980  oeicl  5981  qliftfuns  6126  genprndl  6504  genprndu  6505  nqprloc  6528  ltexprlemrnd  6579  ltexprlemdisj  6580  recexprlemrnd  6601  recexprlemdisj  6602  caucvgprlemlim  6652  negeu  6999  creur  7692  creui  7693  indstr2  8322  iooidg  8548  iccsupr  8605  icoshftf1o  8629  fznlem  8675  frecuzrdgfn  8879  iseqovex  8899  iseqval  8900  iseqfn  8901  iseq1  8902  iseqcl  8903  iseqp1  8904  iseqfveq2  8905  iseqfveq  8907