Theorem ralrimivw 3149

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953

This theorem depends on definitions:  df-bi 199  df-ral 3095

This theorem is referenced by:  2rmorex  3629  riinrab  4829  exse  5319  dmxp  5589  mpt2eq12  6992  ovmpt3rabdm  7169  offveqb  7196  exse2  7384  xpexgALT  7438  opabn1stprc  7507  mpt2exg  7525  uniqs  8090  boxriin  8236  fisupg  8496  fisup2g  8662  fisupcl  8663  fiinfg  8693  fiinf2g  8694  ordtypelem8  8719  wemapso2  8747  cantnflem1  8883  r1val1  8946  scottex  9045  updjud  9093  dfac12k  9304  compssiso  9531  axcclem  9614  ondomon  9720  tskuni  9940  pinq  10084  supexpr  10211  dedekind  10539  supadd  11345  supmullem2  11348  zsupss  12084  qextlt  12346  qextle  12347  xrsupsslem  12449  xrinfmsslem  12450  supxrpnf  12460  ssnn0fi  13103  recan  14483  climconst  14682  sumeq2sdv  14842  dvdsext  15450  smupvallem  15611  smumullem  15620  pc11  15988  prmreclem4  16027  vdwmc2  16087  vdwlem8  16096  vdwlem13  16101  cshwsex  16206  cshws0  16207  prdsplusg  16504  prdsmulr  16505  prdsvsca  16506  prdshom  16513  imasplusg  16563  imasmulr  16564  imasip  16567  imasaddvallem  16575  imasvscaf  16585  quslem  16589  divsfval  16593  mrcuni  16667  catideu  16721  homfeqd  16740  comfeqd  16752  2oppccomf  16770  catcoppccl  17143  lublecllem  17374  pmtrrn  18260  pmtrfrn  18261  gsummptif1n0  18751  evlseu  19912  ip2eq  20396  frlmup4  20544  pmatcollpw2lem  20989  basdif0  21165  clsval2  21262  neif  21312  ordtbaslem  21400  ordtrest2lem  21415  lmconst  21473  cndis  21503  pnrmopn  21555  cmpfi  21620  finptfin  21730  comppfsc  21744  ptbasfi  21793  pttoponconst  21809  ptcnplem  21833  pthaus  21850  xkoptsub  21866  xkopt  21867  nrmr0reg  21961  ordthmeolem  22013  fbssfi  22049  filconn  22095  hausflim  22193  cnpflf  22213  fclscf  22237  cnpfcf  22253  alexsublem  22256  ptcmplem2  22265  ptcmplem3  22266  tsmsfbas  22339  eltsms  22344  utopbas  22447  isucn2  22491  psmetutop  22780  nrginvrcn  22904  lebnumlem3  23170  fmcfil  23478  ovolicc2lem4  23724  mbfconst  23837  i1fmul  23900  itg2const  23944  itg2cnlem2  23966  itgle  24013  ibladdlem  24023  iblabs  24032  iblabsr  24033  iblmulc2  24034  bddmulibl  24042  ellimc2  24078  limcnlp  24079  c1lip1  24197  ply1nzb  24319  ulm0  24582  itgulm2  24600  dchrhash  25448  lgsquadlem2  25558  2sqlem10  25605  dchrisum  25633  rpvmasum2  25653  pntlemj  25744  axcontlem12  26324  nbgr0edg  26704  rusgr1vtx  26936  uspgr2wlkeq2  26994  clwwlknondisj  27513  ip2eqi  28284  ubthlem1  28298  hial2eq  28535  occon  28718  spanss  28779  pjnmopi  29579  ssmd1  29742  chrelat2i  29796  xrofsup  30098  ordtrest2NEWlem  30566  prodindf  30683  truae  30904  mbfmcst  30919  mbfmcnt  30928  dya2iocuni  30943  0rrv  31112  hashreprin  31300  reprgt  31301  breprexplemc  31312  breprexp  31313  circlemeth  31320  hgt750lema  31337  cvmliftlem15  31879  trpredss  32317  neibastop2lem  32943  tailf  32958  filnetlem4  32964  fin2so  34021  matunitlindflem1  34031  matunitlindflem2  34032  poimirlem26  34061  poimirlem28  34063  ismblfin  34076  cnambfre  34083  itg2addnclem  34086  itg2addnc  34089  itg2gt0cn  34090  ibladdnclem  34091  iblabsnc  34099  iblmulc2nc  34100  bddiblnc  34105  ftc1anclem6  34115  ftc1anclem7  34116  ftc1anclem8  34117  ftc1anc  34118  frinfm  34155  sdclem1  34163  ssbnd  34211  rngoueqz  34363  lssatle  35169  ltrneq2  36302  tendoeq2  36928  hbtlem7  38654  itgoss  38692  itgpowd  38758  trclrelexplem  38960  rfovcnvf1od  39254  dssmapf1od  39271  prodeq2ad  40732  0cnv  40882  itgperiod  41124  stoweidlem35  41179  stoweidlem59  41203  fourierdlem31  41282  subsaliuncllem  41499  subsaliuncl  41500  iundjiun  41601  hoiprodcl2  41696  ovnsslelem  41701  ovn0lem  41706  hoidmvlelem3  41738  smflimlem1  41906  smflimlem2  41907  smflimlem3  41908  2reurex  42142  sprval  42418  prprval  42453  rmsupp0  43164  lincop  43212  lcoc0  43226