Theorem ralrimivw 3144

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

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

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 1913

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

This theorem is referenced by:  r19.21v  3173  r19.37v  3175  r19.27v  3181  r19.28v  3183  2rmorex  3703  2reurex  3709  riinrab  5035  exse  5587  dmxp  5874  mpoeq12  7414  ovmpt3rabdm  7594  offveqb  7624  epweon  7691  exse2  7836  xpexgALT  7896  opabn1stprc  7970  mpoexg  7989  uniqs  8641  boxriin  8803  fisupg  9160  fisup2g  9329  fisupcl  9330  fiinfg  9360  fiinf2g  9361  ordtypelem8  9386  wemapso2  9414  cantnflem1  9550  r1val1  9647  updjud  9795  dfac12k  10008  compssiso  10235  axcclem  10318  ondomon  10424  tskuni  10644  pinq  10788  supexpr  10915  dedekind  11243  supadd  12048  supmullem2  12051  zsupss  12782  qextlt  13042  qextle  13043  xrsupsslem  13146  xrinfmsslem  13147  supxrpnf  13157  ssnn0fi  13810  recan  15147  climconst  15351  sumeq2sdv  15515  dvdsext  16129  smupvallem  16289  smumullem  16298  pc11  16678  prmreclem4  16717  vdwmc2  16777  vdwlem8  16786  vdwlem13  16791  cshwsex  16899  cshws0  16900  prdsplusg  17266  prdsmulr  17267  prdsvsca  17268  prdshom  17275  imasplusg  17325  imasmulr  17326  imasip  17329  imasaddvallem  17337  imasvscaf  17347  quslem  17351  divsfval  17355  mrcuni  17427  catideu  17481  homfeqd  17501  comfeqd  17513  2oppccomf  17533  catcoppccl  17929  catcoppcclOLD  17930  lublecllem  18175  pmtrrn  19161  pmtrfrn  19162  gsummptif1n0  19661  ip2eq  20963  frlmup4  21113  evlseu  21398  pmatcollpw2lem  22031  basdif0  22208  clsval2  22306  neif  22356  ordtbaslem  22444  ordtrest2lem  22459  lmconst  22517  cndis  22547  pnrmopn  22599  cmpfi  22664  finptfin  22774  comppfsc  22788  ptbasfi  22837  pttoponconst  22853  ptcnplem  22877  pthaus  22894  xkoptsub  22910  xkopt  22911  nrmr0reg  23005  ordthmeolem  23057  fbssfi  23093  filconn  23139  hausflim  23237  cnpflf  23257  fclscf  23281  cnpfcf  23297  alexsublem  23300  ptcmplem2  23309  ptcmplem3  23310  tsmsfbas  23384  eltsms  23389  utopbas  23492  isucn2  23536  psmetutop  23828  nrginvrcn  23961  lebnumlem3  24231  fmcfil  24541  ovolicc2lem4  24789  mbfconst  24902  i1fmul  24965  itg2const  25010  itg2cnlem2  25032  itgle  25079  ibladdlem  25089  iblabs  25098  iblabsr  25099  iblmulc2  25100  bddmulibl  25108  bddiblnc  25111  ellimc2  25146  limcnlp  25147  c1lip1  25266  itgpowd  25319  ply1nzb  25392  ulm0  25655  itgulm2  25673  dchrhash  26524  lgsquadlem2  26634  2sqlem10  26681  dchrisum  26745  rpvmasum2  26765  pntlemj  26856  bday0b  27074  axcontlem12  27631  nbgr0edg  28012  rusgr1vtx  28243  uspgr2wlkeq2  28302  clwwlknondisj  28762  ip2eqi  29505  ubthlem1  29519  hial2eq  29755  pjnmopi  30797  ssmd1  30960  chrelat2i  31014  xrofsup  31375  ordtrest2NEWlem  32168  prodindf  32287  truae  32507  mbfmcst  32524  mbfmcnt  32533  dya2iocuni  32548  0rrv  32716  hashreprin  32898  reprgt  32899  breprexplemc  32910  breprexp  32911  circlemeth  32918  hgt750lema  32935  cvmliftlem15  33557  satf0suclem  33634  fmla0disjsuc  33657  fmlasucdisj  33658  neibastop2lem  34686  tailf  34701  filnetlem4  34707  fin2so  35920  matunitlindflem1  35929  matunitlindflem2  35930  poimirlem26  35959  poimirlem28  35961  ismblfin  35974  cnambfre  35981  itg2addnclem  35984  itg2addnc  35987  itg2gt0cn  35988  ibladdnclem  35989  iblabsnc  35997  iblmulc2nc  35998  ftc1anclem6  36011  ftc1anclem7  36012  ftc1anclem8  36013  ftc1anc  36014  frinfm  36049  sdclem1  36057  ssbnd  36102  rngoueqz  36254  lssatle  37333  ltrneq2  38467  tendoeq2  39093  lcmineqlem12  40353  hbtlem7  41264  trclrelexplem  41692  rfovcnvf1od  41985  dssmapf1od  42002  neik0pk1imk0  42030  collexd  42248  prodeq2ad  43521  0cnv  43671  itgperiod  43910  stoweidlem35  43964  stoweidlem59  43988  fourierdlem31  44067  subsaliuncllem  44284  subsaliuncl  44285  iundjiun  44387  hoiprodcl2  44482  ovn0lem  44492  hoidmvlelem3  44524  smflimlem1  44698  smflimlem2  44699  smflimlem3  44700  fundcmpsurinjlem2  45269  sprval  45349  prprval  45384  rmsupp0  46122  lincop  46167  lcoc0  46181