Theorem ralrimivw 3147

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

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

This theorem is referenced by:  r19.21v  3177  r19.37v  3179  r19.27v  3185  r19.28v  3187  2rmorex  3762  2reurex  3768  riinrab  5088  exse  5648  dmxpOLD  5942  mpoeq12  7505  ovmpt3rabdm  7691  offveqb  7723  epweon  7793  exse2  7939  xpexgALT  8004  opabn1stprc  8081  mpoexg  8099  uniqs  8815  boxriin  8978  fisupg  9321  fisup2g  9505  fisupcl  9506  fiinfg  9536  fiinf2g  9537  ordtypelem8  9562  wemapso2  9590  cantnflem1  9726  r1val1  9823  updjud  9971  dfac12k  10185  compssiso  10411  axcclem  10494  ondomon  10600  tskuni  10820  pinq  10964  supexpr  11091  dedekind  11421  supadd  12233  supmullem2  12236  zsupss  12976  qextlt  13241  qextle  13242  xrsupsslem  13345  xrinfmsslem  13346  supxrpnf  13356  ssnn0fi  14022  recan  15371  climconst  15575  sumeq2sdvOLD  15736  dvdsext  16354  smupvallem  16516  smumullem  16525  pc11  16913  prmreclem4  16952  vdwmc2  17012  vdwlem8  17021  vdwlem13  17026  cshwsex  17134  cshws0  17135  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  prdshom  17513  imasplusg  17563  imasmulr  17564  imasip  17567  imasaddvallem  17575  imasvscaf  17585  quslem  17589  divsfval  17593  mrcuni  17665  catideu  17719  homfeqd  17739  comfeqd  17751  2oppccomf  17771  catcoppccl  18170  catcoppcclOLD  18171  lublecllem  18417  pmtrrn  19489  pmtrfrn  19490  gsummptif1n0  19998  ip2eq  21688  frlmup4  21838  evlseu  22124  pmatcollpw2lem  22798  basdif0  22975  clsval2  23073  neif  23123  ordtbaslem  23211  ordtrest2lem  23226  lmconst  23284  cndis  23314  pnrmopn  23366  cmpfi  23431  finptfin  23541  comppfsc  23555  ptbasfi  23604  pttoponconst  23620  ptcnplem  23644  pthaus  23661  xkoptsub  23677  xkopt  23678  nrmr0reg  23772  ordthmeolem  23824  fbssfi  23860  filconn  23906  hausflim  24004  cnpflf  24024  fclscf  24048  cnpfcf  24064  alexsublem  24067  ptcmplem2  24076  ptcmplem3  24077  tsmsfbas  24151  eltsms  24156  utopbas  24259  isucn2  24303  psmetutop  24595  nrginvrcn  24728  lebnumlem3  25008  fmcfil  25319  ovolicc2lem4  25568  mbfconst  25681  i1fmul  25744  itg2const  25789  itg2cnlem2  25811  itgle  25859  ibladdlem  25869  iblabs  25878  iblabsr  25879  iblmulc2  25880  bddmulibl  25888  bddiblnc  25891  ellimc2  25926  limcnlp  25927  c1lip1  26050  itgpowd  26105  ply1nzb  26176  ulm0  26448  itgulm2  26466  dchrhash  27329  lgsquadlem2  27439  2sqlem10  27486  dchrisum  27550  rpvmasum2  27570  pntlemj  27661  bday0b  27889  axcontlem12  29004  nbgr0edg  29388  rusgr1vtx  29620  uspgr2wlkeq2  29679  clwwlknondisj  30139  ip2eqi  30884  ubthlem1  30898  hial2eq  31134  pjnmopi  32176  ssmd1  32339  chrelat2i  32393  xrofsup  32777  ordtrest2NEWlem  33882  prodindf  34003  truae  34223  mbfmcst  34240  mbfmcnt  34249  dya2iocuni  34264  0rrv  34432  hashreprin  34613  reprgt  34614  breprexplemc  34625  breprexp  34626  circlemeth  34633  hgt750lema  34650  wevgblacfn  35092  cvmliftlem15  35282  satf0suclem  35359  fmla0disjsuc  35382  fmlasucdisj  35383  neibastop2lem  36342  tailf  36357  filnetlem4  36363  fin2so  37593  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem26  37632  poimirlem28  37634  ismblfin  37647  cnambfre  37654  itg2addnclem  37657  itg2addnc  37660  itg2gt0cn  37661  ibladdnclem  37662  iblabsnc  37670  iblmulc2nc  37671  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  frinfm  37721  sdclem1  37729  ssbnd  37774  rngoueqz  37926  lssatle  38996  ltrneq2  40130  tendoeq2  40756  lcmineqlem12  42021  hbtlem7  43113  trclrelexplem  43700  rfovcnvf1od  43993  dssmapf1od  44010  neik0pk1imk0  44036  collexd  44252  prodeq2ad  45547  0cnv  45697  itgperiod  45936  stoweidlem35  45990  stoweidlem59  46014  fourierdlem31  46093  subsaliuncllem  46312  subsaliuncl  46313  iundjiun  46415  hoiprodcl2  46510  ovn0lem  46520  hoidmvlelem3  46552  smflimlem1  46726  smflimlem2  46727  smflimlem3  46728  fundcmpsurinjlem2  47323  sprval  47403  prprval  47438  rmsupp0  48212  lincop  48253  lcoc0  48267