Theorem ralrimivw 3149

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
ralrimivw.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ralrimivw	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimivw

Step	Hyp	Ref	Expression
1		ralrimivw.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralrimiv 3144	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2105  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912

This theorem depends on definitions:  df-bi 206  df-ral 3061

This theorem is referenced by:  r19.21v  3178  r19.37v  3180  r19.27v  3186  r19.28v  3188  2rmorex  3751  2reurex  3757  riinrab  5088  exse  5640  dmxp  5929  mpoeq12  7485  ovmpt3rabdm  7668  offveqb  7698  epweon  7765  exse2  7911  xpexgALT  7971  opabn1stprc  8047  mpoexg  8066  uniqs  8774  boxriin  8937  fisupg  9294  fisup2g  9466  fisupcl  9467  fiinfg  9497  fiinf2g  9498  ordtypelem8  9523  wemapso2  9551  cantnflem1  9687  r1val1  9784  updjud  9932  dfac12k  10145  compssiso  10372  axcclem  10455  ondomon  10561  tskuni  10781  pinq  10925  supexpr  11052  dedekind  11382  supadd  12187  supmullem2  12190  zsupss  12926  qextlt  13187  qextle  13188  xrsupsslem  13291  xrinfmsslem  13292  supxrpnf  13302  ssnn0fi  13955  recan  15288  climconst  15492  sumeq2sdv  15655  dvdsext  16269  smupvallem  16429  smumullem  16438  pc11  16818  prmreclem4  16857  vdwmc2  16917  vdwlem8  16926  vdwlem13  16931  cshwsex  17039  cshws0  17040  prdsplusg  17409  prdsmulr  17410  prdsvsca  17411  prdshom  17418  imasplusg  17468  imasmulr  17469  imasip  17472  imasaddvallem  17480  imasvscaf  17490  quslem  17494  divsfval  17498  mrcuni  17570  catideu  17624  homfeqd  17644  comfeqd  17656  2oppccomf  17676  catcoppccl  18072  catcoppcclOLD  18073  lublecllem  18318  pmtrrn  19367  pmtrfrn  19368  gsummptif1n0  19876  ip2eq  21426  frlmup4  21576  evlseu  21866  pmatcollpw2lem  22500  basdif0  22677  clsval2  22775  neif  22825  ordtbaslem  22913  ordtrest2lem  22928  lmconst  22986  cndis  23016  pnrmopn  23068  cmpfi  23133  finptfin  23243  comppfsc  23257  ptbasfi  23306  pttoponconst  23322  ptcnplem  23346  pthaus  23363  xkoptsub  23379  xkopt  23380  nrmr0reg  23474  ordthmeolem  23526  fbssfi  23562  filconn  23608  hausflim  23706  cnpflf  23726  fclscf  23750  cnpfcf  23766  alexsublem  23769  ptcmplem2  23778  ptcmplem3  23779  tsmsfbas  23853  eltsms  23858  utopbas  23961  isucn2  24005  psmetutop  24297  nrginvrcn  24430  lebnumlem3  24710  fmcfil  25021  ovolicc2lem4  25270  mbfconst  25383  i1fmul  25446  itg2const  25491  itg2cnlem2  25513  itgle  25560  ibladdlem  25570  iblabs  25579  iblabsr  25580  iblmulc2  25581  bddmulibl  25589  bddiblnc  25592  ellimc2  25627  limcnlp  25628  c1lip1  25747  itgpowd  25800  ply1nzb  25873  ulm0  26136  itgulm2  26154  dchrhash  27007  lgsquadlem2  27117  2sqlem10  27164  dchrisum  27228  rpvmasum2  27248  pntlemj  27339  bday0b  27565  axcontlem12  28497  nbgr0edg  28878  rusgr1vtx  29109  uspgr2wlkeq2  29168  clwwlknondisj  29628  ip2eqi  30373  ubthlem1  30387  hial2eq  30623  pjnmopi  31665  ssmd1  31828  chrelat2i  31882  xrofsup  32244  ordtrest2NEWlem  33197  prodindf  33316  truae  33536  mbfmcst  33553  mbfmcnt  33562  dya2iocuni  33577  0rrv  33745  hashreprin  33927  reprgt  33928  breprexplemc  33939  breprexp  33940  circlemeth  33947  hgt750lema  33964  cvmliftlem15  34584  satf0suclem  34661  fmla0disjsuc  34684  fmlasucdisj  34685  neibastop2lem  35549  tailf  35564  filnetlem4  35570  fin2so  36779  matunitlindflem1  36788  matunitlindflem2  36789  poimirlem26  36818  poimirlem28  36820  ismblfin  36833  cnambfre  36840  itg2addnclem  36843  itg2addnc  36846  itg2gt0cn  36847  ibladdnclem  36848  iblabsnc  36856  iblmulc2nc  36857  ftc1anclem6  36870  ftc1anclem7  36871  ftc1anclem8  36872  ftc1anc  36873  frinfm  36907  sdclem1  36915  ssbnd  36960  rngoueqz  37112  lssatle  38189  ltrneq2  39323  tendoeq2  39949  lcmineqlem12  41212  hbtlem7  42170  trclrelexplem  42765  rfovcnvf1od  43058  dssmapf1od  43075  neik0pk1imk0  43101  collexd  43319  prodeq2ad  44608  0cnv  44758  itgperiod  44997  stoweidlem35  45051  stoweidlem59  45075  fourierdlem31  45154  subsaliuncllem  45373  subsaliuncl  45374  iundjiun  45476  hoiprodcl2  45571  ovn0lem  45581  hoidmvlelem3  45613  smflimlem1  45787  smflimlem2  45788  smflimlem3  45789  fundcmpsurinjlem2  46367  sprval  46447  prprval  46482  rmsupp0  47134  lincop  47178  lcoc0  47192