Theorem ralrimivw 3134

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3052

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

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

This theorem is referenced by:  r19.21v  3163  r19.37v  3164  r19.27v  3167  r19.28v  3169  2rmorex  3714  2reurex  3720  riinrab  5041  exse  5594  mpoeq12  7443  ovmpt3rabdm  7629  offveqb  7661  epweon  7732  exse2  7871  xpexgALT  7937  opabn1stprc  8014  mpoexg  8032  boxriin  8892  fisupg  9202  fisup2g  9386  fisupcl  9387  fiinfg  9418  fiinf2g  9419  ordtypelem8  9444  wemapso2  9472  cantnflem1  9612  r1val1  9712  updjud  9860  dfac12k  10072  compssiso  10298  axcclem  10381  ondomon  10487  tskuni  10708  pinq  10852  supexpr  10979  dedekind  11310  supadd  12124  supmullem2  12127  zsupss  12864  qextlt  13132  qextle  13133  xrsupsslem  13236  xrinfmsslem  13237  supxrpnf  13247  ssnn0fi  13922  recan  15274  climconst  15480  sumeq2sdvOLD  15641  dvdsext  16262  smupvallem  16424  smumullem  16433  pc11  16822  prmreclem4  16861  vdwmc2  16921  vdwlem8  16930  vdwlem13  16935  cshwsex  17042  cshws0  17043  prdsplusg  17392  prdsmulr  17393  prdsvsca  17394  prdshom  17401  imasplusg  17452  imasmulr  17453  imasip  17456  imasaddvallem  17464  imasvscaf  17474  quslem  17478  divsfval  17482  mrcuni  17558  catideu  17612  homfeqd  17632  comfeqd  17644  2oppccomf  17662  catcoppccl  18055  lublecllem  18295  chnfi  18571  pmtrrn  19403  pmtrfrn  19404  gsummptif1n0  19912  ip2eq  21625  frlmup4  21773  evlseu  22055  pmatcollpw2lem  22738  basdif0  22914  clsval2  23011  neif  23061  ordtbaslem  23149  ordtrest2lem  23164  lmconst  23222  cndis  23252  pnrmopn  23304  cmpfi  23369  finptfin  23479  comppfsc  23493  ptbasfi  23542  pttoponconst  23558  ptcnplem  23582  pthaus  23599  xkoptsub  23615  xkopt  23616  nrmr0reg  23710  ordthmeolem  23762  fbssfi  23798  filconn  23844  hausflim  23942  cnpflf  23962  fclscf  23986  cnpfcf  24002  alexsublem  24005  ptcmplem2  24014  ptcmplem3  24015  tsmsfbas  24089  eltsms  24094  utopbas  24196  isucn2  24239  psmetutop  24528  nrginvrcn  24653  lebnumlem3  24935  fmcfil  25245  ovolicc2lem4  25494  mbfconst  25607  i1fmul  25670  itg2const  25714  itg2cnlem2  25736  itgle  25784  ibladdlem  25794  iblabs  25803  iblabsr  25804  iblmulc2  25805  bddmulibl  25813  bddiblnc  25816  ellimc2  25851  limcnlp  25852  c1lip1  25975  itgpowd  26030  ply1nzb  26101  ulm0  26373  itgulm2  26391  dchrhash  27255  lgsquadlem2  27365  2sqlem10  27412  dchrisum  27476  rpvmasum2  27496  pntlemj  27587  bday0b  27826  axcontlem12  29066  nbgr0edg  29448  rusgr1vtx  29680  uspgr2wlkeq2  29738  clwwlknondisj  30204  ip2eqi  30950  ubthlem1  30964  hial2eq  31200  pjnmopi  32242  ssmd1  32405  chrelat2i  32459  xrofsup  32864  prodindf  32961  extdgfialglem2  33877  ordtrest2NEWlem  34106  truae  34427  mbfmcst  34443  mbfmcnt  34452  dya2iocuni  34467  0rrv  34635  hashreprin  34804  reprgt  34805  breprexplemc  34816  breprexp  34817  circlemeth  34824  hgt750lema  34841  fineqvnttrclselem1  35305  fineqvnttrclse  35308  vonf1owev  35330  wevgblacfn  35331  cvmliftlem15  35520  satf0suclem  35597  fmla0disjsuc  35620  fmlasucdisj  35621  neibastop2lem  36582  tailf  36597  filnetlem4  36603  fin2so  37887  matunitlindflem1  37896  matunitlindflem2  37897  poimirlem26  37926  poimirlem28  37928  ismblfin  37941  cnambfre  37948  itg2addnclem  37951  itg2addnc  37954  itg2gt0cn  37955  ibladdnclem  37956  iblabsnc  37964  iblmulc2nc  37965  ftc1anclem6  37978  ftc1anclem7  37979  ftc1anclem8  37980  ftc1anc  37981  frinfm  38015  sdclem1  38023  ssbnd  38068  rngoueqz  38220  lssatle  39420  ltrneq2  40553  tendoeq2  41179  lcmineqlem12  42439  hbtlem7  43511  trclrelexplem  44096  rfovcnvf1od  44389  dssmapf1od  44406  neik0pk1imk0  44432  collexd  44642  sswfaxreg  45372  omssaxinf2  45373  prodeq2ad  45981  0cnv  46129  itgperiod  46368  stoweidlem35  46422  stoweidlem59  46446  fourierdlem31  46525  subsaliuncllem  46744  subsaliuncl  46745  iundjiun  46847  hoiprodcl2  46942  ovn0lem  46952  hoidmvlelem3  46984  smflimlem1  47158  smflimlem2  47159  smflimlem3  47160  fundcmpsurinjlem2  47788  sprval  47868  prprval  47903  rmsupp0  48757  lincop  48797  lcoc0  48811  nelsubclem  49455