Theorem ralrimivw 3151

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

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

This theorem is referenced by:  r19.21v  3180  r19.37v  3182  r19.27v  3188  r19.28v  3190  2rmorex  3750  2reurex  3756  riinrab  5087  exse  5639  dmxp  5927  mpoeq12  7479  ovmpt3rabdm  7662  offveqb  7692  epweon  7759  exse2  7905  xpexgALT  7965  opabn1stprc  8041  mpoexg  8060  uniqs  8768  boxriin  8931  fisupg  9288  fisup2g  9460  fisupcl  9461  fiinfg  9491  fiinf2g  9492  ordtypelem8  9517  wemapso2  9545  cantnflem1  9681  r1val1  9778  updjud  9926  dfac12k  10139  compssiso  10366  axcclem  10449  ondomon  10555  tskuni  10775  pinq  10919  supexpr  11046  dedekind  11374  supadd  12179  supmullem2  12182  zsupss  12918  qextlt  13179  qextle  13180  xrsupsslem  13283  xrinfmsslem  13284  supxrpnf  13294  ssnn0fi  13947  recan  15280  climconst  15484  sumeq2sdv  15647  dvdsext  16261  smupvallem  16421  smumullem  16430  pc11  16810  prmreclem4  16849  vdwmc2  16909  vdwlem8  16918  vdwlem13  16923  cshwsex  17031  cshws0  17032  prdsplusg  17401  prdsmulr  17402  prdsvsca  17403  prdshom  17410  imasplusg  17460  imasmulr  17461  imasip  17464  imasaddvallem  17472  imasvscaf  17482  quslem  17486  divsfval  17490  mrcuni  17562  catideu  17616  homfeqd  17636  comfeqd  17648  2oppccomf  17668  catcoppccl  18064  catcoppcclOLD  18065  lublecllem  18310  pmtrrn  19320  pmtrfrn  19321  gsummptif1n0  19829  ip2eq  21198  frlmup4  21348  evlseu  21638  pmatcollpw2lem  22271  basdif0  22448  clsval2  22546  neif  22596  ordtbaslem  22684  ordtrest2lem  22699  lmconst  22757  cndis  22787  pnrmopn  22839  cmpfi  22904  finptfin  23014  comppfsc  23028  ptbasfi  23077  pttoponconst  23093  ptcnplem  23117  pthaus  23134  xkoptsub  23150  xkopt  23151  nrmr0reg  23245  ordthmeolem  23297  fbssfi  23333  filconn  23379  hausflim  23477  cnpflf  23497  fclscf  23521  cnpfcf  23537  alexsublem  23540  ptcmplem2  23549  ptcmplem3  23550  tsmsfbas  23624  eltsms  23629  utopbas  23732  isucn2  23776  psmetutop  24068  nrginvrcn  24201  lebnumlem3  24471  fmcfil  24781  ovolicc2lem4  25029  mbfconst  25142  i1fmul  25205  itg2const  25250  itg2cnlem2  25272  itgle  25319  ibladdlem  25329  iblabs  25338  iblabsr  25339  iblmulc2  25340  bddmulibl  25348  bddiblnc  25351  ellimc2  25386  limcnlp  25387  c1lip1  25506  itgpowd  25559  ply1nzb  25632  ulm0  25895  itgulm2  25913  dchrhash  26764  lgsquadlem2  26874  2sqlem10  26921  dchrisum  26985  rpvmasum2  27005  pntlemj  27096  bday0b  27321  axcontlem12  28223  nbgr0edg  28604  rusgr1vtx  28835  uspgr2wlkeq2  28894  clwwlknondisj  29354  ip2eqi  30097  ubthlem1  30111  hial2eq  30347  pjnmopi  31389  ssmd1  31552  chrelat2i  31606  xrofsup  31968  ordtrest2NEWlem  32891  prodindf  33010  truae  33230  mbfmcst  33247  mbfmcnt  33256  dya2iocuni  33271  0rrv  33439  hashreprin  33621  reprgt  33622  breprexplemc  33633  breprexp  33634  circlemeth  33641  hgt750lema  33658  cvmliftlem15  34278  satf0suclem  34355  fmla0disjsuc  34378  fmlasucdisj  34379  neibastop2lem  35234  tailf  35249  filnetlem4  35255  fin2so  36464  matunitlindflem1  36473  matunitlindflem2  36474  poimirlem26  36503  poimirlem28  36505  ismblfin  36518  cnambfre  36525  itg2addnclem  36528  itg2addnc  36531  itg2gt0cn  36532  ibladdnclem  36533  iblabsnc  36541  iblmulc2nc  36542  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  frinfm  36592  sdclem1  36600  ssbnd  36645  rngoueqz  36797  lssatle  37874  ltrneq2  39008  tendoeq2  39634  lcmineqlem12  40894  hbtlem7  41853  trclrelexplem  42448  rfovcnvf1od  42741  dssmapf1od  42758  neik0pk1imk0  42784  collexd  43002  prodeq2ad  44295  0cnv  44445  itgperiod  44684  stoweidlem35  44738  stoweidlem59  44762  fourierdlem31  44841  subsaliuncllem  45060  subsaliuncl  45061  iundjiun  45163  hoiprodcl2  45258  ovn0lem  45268  hoidmvlelem3  45300  smflimlem1  45474  smflimlem2  45475  smflimlem3  45476  fundcmpsurinjlem2  46054  sprval  46134  prprval  46169  rmsupp0  46998  lincop  47043  lcoc0  47057