Theorem ralrimivw 3108

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3063

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

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

This theorem is referenced by:  r19.27v  3109  r19.28v  3110  r19.37v  3271  2rmorex  3684  2reurex  3690  riinrab  5009  exse  5543  dmxp  5827  mpoeq12  7326  ovmpt3rabdm  7506  offveqb  7536  exse2  7738  xpexgALT  7797  opabn1stprc  7871  mpoexg  7890  uniqs  8524  boxriin  8686  fisupg  8992  fisup2g  9157  fisupcl  9158  fiinfg  9188  fiinf2g  9189  ordtypelem8  9214  wemapso2  9242  cantnflem1  9377  trpredss  9407  r1val1  9475  scottex  9574  updjud  9623  dfac12k  9834  compssiso  10061  axcclem  10144  ondomon  10250  tskuni  10470  pinq  10614  supexpr  10741  dedekind  11068  supadd  11873  supmullem2  11876  zsupss  12606  qextlt  12866  qextle  12867  xrsupsslem  12970  xrinfmsslem  12971  supxrpnf  12981  ssnn0fi  13633  recan  14976  climconst  15180  sumeq2sdv  15344  dvdsext  15958  smupvallem  16118  smumullem  16127  pc11  16509  prmreclem4  16548  vdwmc2  16608  vdwlem8  16617  vdwlem13  16622  cshwsex  16730  cshws0  16731  prdsplusg  17086  prdsmulr  17087  prdsvsca  17088  prdshom  17095  imasplusg  17145  imasmulr  17146  imasip  17149  imasaddvallem  17157  imasvscaf  17167  quslem  17171  divsfval  17175  mrcuni  17247  catideu  17301  homfeqd  17321  comfeqd  17333  2oppccomf  17353  catcoppccl  17748  catcoppcclOLD  17749  lublecllem  17993  pmtrrn  18980  pmtrfrn  18981  gsummptif1n0  19482  ip2eq  20770  frlmup4  20918  evlseu  21203  pmatcollpw2lem  21834  basdif0  22011  clsval2  22109  neif  22159  ordtbaslem  22247  ordtrest2lem  22262  lmconst  22320  cndis  22350  pnrmopn  22402  cmpfi  22467  finptfin  22577  comppfsc  22591  ptbasfi  22640  pttoponconst  22656  ptcnplem  22680  pthaus  22697  xkoptsub  22713  xkopt  22714  nrmr0reg  22808  ordthmeolem  22860  fbssfi  22896  filconn  22942  hausflim  23040  cnpflf  23060  fclscf  23084  cnpfcf  23100  alexsublem  23103  ptcmplem2  23112  ptcmplem3  23113  tsmsfbas  23187  eltsms  23192  utopbas  23295  isucn2  23339  psmetutop  23629  nrginvrcn  23762  lebnumlem3  24032  fmcfil  24341  ovolicc2lem4  24589  mbfconst  24702  i1fmul  24765  itg2const  24810  itg2cnlem2  24832  itgle  24879  ibladdlem  24889  iblabs  24898  iblabsr  24899  iblmulc2  24900  bddmulibl  24908  bddiblnc  24911  ellimc2  24946  limcnlp  24947  c1lip1  25066  itgpowd  25119  ply1nzb  25192  ulm0  25455  itgulm2  25473  dchrhash  26324  lgsquadlem2  26434  2sqlem10  26481  dchrisum  26545  rpvmasum2  26565  pntlemj  26656  axcontlem12  27246  nbgr0edg  27627  rusgr1vtx  27858  uspgr2wlkeq2  27916  clwwlknondisj  28376  ip2eqi  29119  ubthlem1  29133  hial2eq  29369  occon  29550  spanss  29611  pjnmopi  30411  ssmd1  30574  chrelat2i  30628  xrofsup  30992  ordtrest2NEWlem  31774  prodindf  31891  truae  32111  mbfmcst  32126  mbfmcnt  32135  dya2iocuni  32150  0rrv  32318  hashreprin  32500  reprgt  32501  breprexplemc  32512  breprexp  32513  circlemeth  32520  hgt750lema  32537  cvmliftlem15  33160  satf0suclem  33237  fmla0disjsuc  33260  fmlasucdisj  33261  bday0b  33951  neibastop2lem  34476  tailf  34491  filnetlem4  34497  fin2so  35691  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem26  35730  poimirlem28  35732  ismblfin  35745  cnambfre  35752  itg2addnclem  35755  itg2addnc  35758  itg2gt0cn  35759  ibladdnclem  35760  iblabsnc  35768  iblmulc2nc  35769  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  frinfm  35820  sdclem1  35828  ssbnd  35873  rngoueqz  36025  lssatle  36956  ltrneq2  38089  tendoeq2  38715  lcmineqlem12  39976  hbtlem7  40866  itgoss  40904  trclrelexplem  41208  rfovcnvf1od  41501  dssmapf1od  41518  neik0pk1imk0  41546  collexd  41764  prodeq2ad  43023  0cnv  43173  itgperiod  43412  stoweidlem35  43466  stoweidlem59  43490  fourierdlem31  43569  subsaliuncllem  43786  subsaliuncl  43787  iundjiun  43888  hoiprodcl2  43983  ovnsslelem  43988  ovn0lem  43993  hoidmvlelem3  44025  smflimlem1  44193  smflimlem2  44194  smflimlem3  44195  fundcmpsurinjlem2  44739  sprval  44819  prprval  44854  rmsupp0  45592  lincop  45637  lcoc0  45651