Theorem ralrimivw 3128

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 3123	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3047

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 1911

This theorem depends on definitions:  df-bi 207  df-ral 3048

This theorem is referenced by:  r19.21v  3157  r19.37v  3158  r19.27v  3161  r19.28v  3163  2rmorex  3708  2reurex  3714  riinrab  5030  exse  5574  mpoeq12  7419  ovmpt3rabdm  7605  offveqb  7637  epweon  7708  exse2  7847  xpexgALT  7913  opabn1stprc  7990  mpoexg  8008  boxriin  8864  fisupg  9172  fisup2g  9353  fisupcl  9354  fiinfg  9385  fiinf2g  9386  ordtypelem8  9411  wemapso2  9439  cantnflem1  9579  r1val1  9679  updjud  9827  dfac12k  10039  compssiso  10265  axcclem  10348  ondomon  10454  tskuni  10674  pinq  10818  supexpr  10945  dedekind  11276  supadd  12090  supmullem2  12093  zsupss  12835  qextlt  13102  qextle  13103  xrsupsslem  13206  xrinfmsslem  13207  supxrpnf  13217  ssnn0fi  13892  recan  15244  climconst  15450  sumeq2sdvOLD  15611  dvdsext  16232  smupvallem  16394  smumullem  16403  pc11  16792  prmreclem4  16831  vdwmc2  16891  vdwlem8  16900  vdwlem13  16905  cshwsex  17012  cshws0  17013  prdsplusg  17362  prdsmulr  17363  prdsvsca  17364  prdshom  17371  imasplusg  17421  imasmulr  17422  imasip  17425  imasaddvallem  17433  imasvscaf  17443  quslem  17447  divsfval  17451  mrcuni  17527  catideu  17581  homfeqd  17601  comfeqd  17613  2oppccomf  17631  catcoppccl  18024  lublecllem  18264  chnfi  18540  pmtrrn  19369  pmtrfrn  19370  gsummptif1n0  19878  ip2eq  21590  frlmup4  21738  evlseu  22018  pmatcollpw2lem  22692  basdif0  22868  clsval2  22965  neif  23015  ordtbaslem  23103  ordtrest2lem  23118  lmconst  23176  cndis  23206  pnrmopn  23258  cmpfi  23323  finptfin  23433  comppfsc  23447  ptbasfi  23496  pttoponconst  23512  ptcnplem  23536  pthaus  23553  xkoptsub  23569  xkopt  23570  nrmr0reg  23664  ordthmeolem  23716  fbssfi  23752  filconn  23798  hausflim  23896  cnpflf  23916  fclscf  23940  cnpfcf  23956  alexsublem  23959  ptcmplem2  23968  ptcmplem3  23969  tsmsfbas  24043  eltsms  24048  utopbas  24150  isucn2  24193  psmetutop  24482  nrginvrcn  24607  lebnumlem3  24889  fmcfil  25199  ovolicc2lem4  25448  mbfconst  25561  i1fmul  25624  itg2const  25668  itg2cnlem2  25690  itgle  25738  ibladdlem  25748  iblabs  25757  iblabsr  25758  iblmulc2  25759  bddmulibl  25767  bddiblnc  25770  ellimc2  25805  limcnlp  25806  c1lip1  25929  itgpowd  25984  ply1nzb  26055  ulm0  26327  itgulm2  26345  dchrhash  27209  lgsquadlem2  27319  2sqlem10  27366  dchrisum  27430  rpvmasum2  27450  pntlemj  27541  bday0b  27774  axcontlem12  28953  nbgr0edg  29335  rusgr1vtx  29567  uspgr2wlkeq2  29625  clwwlknondisj  30091  ip2eqi  30836  ubthlem1  30850  hial2eq  31086  pjnmopi  32128  ssmd1  32291  chrelat2i  32345  xrofsup  32750  prodindf  32844  extdgfialglem2  33706  ordtrest2NEWlem  33935  truae  34256  mbfmcst  34272  mbfmcnt  34281  dya2iocuni  34296  0rrv  34464  hashreprin  34633  reprgt  34634  breprexplemc  34645  breprexp  34646  circlemeth  34653  hgt750lema  34670  fineqvnttrclselem1  35141  fineqvnttrclse  35144  vonf1owev  35152  wevgblacfn  35153  cvmliftlem15  35342  satf0suclem  35419  fmla0disjsuc  35442  fmlasucdisj  35443  neibastop2lem  36404  tailf  36419  filnetlem4  36425  fin2so  37646  matunitlindflem1  37655  matunitlindflem2  37656  poimirlem26  37685  poimirlem28  37687  ismblfin  37700  cnambfre  37707  itg2addnclem  37710  itg2addnc  37713  itg2gt0cn  37714  ibladdnclem  37715  iblabsnc  37723  iblmulc2nc  37724  ftc1anclem6  37737  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  frinfm  37774  sdclem1  37782  ssbnd  37827  rngoueqz  37979  lssatle  39113  ltrneq2  40246  tendoeq2  40872  lcmineqlem12  42132  hbtlem7  43217  trclrelexplem  43803  rfovcnvf1od  44096  dssmapf1od  44113  neik0pk1imk0  44139  collexd  44349  sswfaxreg  45079  omssaxinf2  45080  prodeq2ad  45691  0cnv  45839  itgperiod  46078  stoweidlem35  46132  stoweidlem59  46156  fourierdlem31  46235  subsaliuncllem  46454  subsaliuncl  46455  iundjiun  46557  hoiprodcl2  46652  ovn0lem  46662  hoidmvlelem3  46694  smflimlem1  46868  smflimlem2  46869  smflimlem3  46870  fundcmpsurinjlem2  47498  sprval  47578  prprval  47613  rmsupp0  48467  lincop  48508  lcoc0  48522  nelsubclem  49167