Theorem ralrimivw 3104

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

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

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 1913

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

This theorem is referenced by:  r19.21v  3113  r19.27v  3115  r19.28v  3116  r19.37v  3274  2rmorex  3689  2reurex  3695  riinrab  5013  exse  5552  dmxp  5838  mpoeq12  7348  ovmpt3rabdm  7528  offveqb  7558  epweon  7625  exse2  7764  xpexgALT  7824  opabn1stprc  7898  mpoexg  7917  uniqs  8566  boxriin  8728  fisupg  9062  fisup2g  9227  fisupcl  9228  fiinfg  9258  fiinf2g  9259  ordtypelem8  9284  wemapso2  9312  cantnflem1  9447  r1val1  9544  scottex  9643  updjud  9692  dfac12k  9903  compssiso  10130  axcclem  10213  ondomon  10319  tskuni  10539  pinq  10683  supexpr  10810  dedekind  11138  supadd  11943  supmullem2  11946  zsupss  12677  qextlt  12937  qextle  12938  xrsupsslem  13041  xrinfmsslem  13042  supxrpnf  13052  ssnn0fi  13705  recan  15048  climconst  15252  sumeq2sdv  15416  dvdsext  16030  smupvallem  16190  smumullem  16199  pc11  16581  prmreclem4  16620  vdwmc2  16680  vdwlem8  16689  vdwlem13  16694  cshwsex  16802  cshws0  16803  prdsplusg  17169  prdsmulr  17170  prdsvsca  17171  prdshom  17178  imasplusg  17228  imasmulr  17229  imasip  17232  imasaddvallem  17240  imasvscaf  17250  quslem  17254  divsfval  17258  mrcuni  17330  catideu  17384  homfeqd  17404  comfeqd  17416  2oppccomf  17436  catcoppccl  17832  catcoppcclOLD  17833  lublecllem  18078  pmtrrn  19065  pmtrfrn  19066  gsummptif1n0  19567  ip2eq  20858  frlmup4  21008  evlseu  21293  pmatcollpw2lem  21926  basdif0  22103  clsval2  22201  neif  22251  ordtbaslem  22339  ordtrest2lem  22354  lmconst  22412  cndis  22442  pnrmopn  22494  cmpfi  22559  finptfin  22669  comppfsc  22683  ptbasfi  22732  pttoponconst  22748  ptcnplem  22772  pthaus  22789  xkoptsub  22805  xkopt  22806  nrmr0reg  22900  ordthmeolem  22952  fbssfi  22988  filconn  23034  hausflim  23132  cnpflf  23152  fclscf  23176  cnpfcf  23192  alexsublem  23195  ptcmplem2  23204  ptcmplem3  23205  tsmsfbas  23279  eltsms  23284  utopbas  23387  isucn2  23431  psmetutop  23723  nrginvrcn  23856  lebnumlem3  24126  fmcfil  24436  ovolicc2lem4  24684  mbfconst  24797  i1fmul  24860  itg2const  24905  itg2cnlem2  24927  itgle  24974  ibladdlem  24984  iblabs  24993  iblabsr  24994  iblmulc2  24995  bddmulibl  25003  bddiblnc  25006  ellimc2  25041  limcnlp  25042  c1lip1  25161  itgpowd  25214  ply1nzb  25287  ulm0  25550  itgulm2  25568  dchrhash  26419  lgsquadlem2  26529  2sqlem10  26576  dchrisum  26640  rpvmasum2  26660  pntlemj  26751  axcontlem12  27343  nbgr0edg  27724  rusgr1vtx  27955  uspgr2wlkeq2  28014  clwwlknondisj  28475  ip2eqi  29218  ubthlem1  29232  hial2eq  29468  occon  29649  spanss  29710  pjnmopi  30510  ssmd1  30673  chrelat2i  30727  xrofsup  31090  ordtrest2NEWlem  31872  prodindf  31991  truae  32211  mbfmcst  32226  mbfmcnt  32235  dya2iocuni  32250  0rrv  32418  hashreprin  32600  reprgt  32601  breprexplemc  32612  breprexp  32613  circlemeth  32620  hgt750lema  32637  cvmliftlem15  33260  satf0suclem  33337  fmla0disjsuc  33360  fmlasucdisj  33361  bday0b  34024  neibastop2lem  34549  tailf  34564  filnetlem4  34570  fin2so  35764  matunitlindflem1  35773  matunitlindflem2  35774  poimirlem26  35803  poimirlem28  35805  ismblfin  35818  cnambfre  35825  itg2addnclem  35828  itg2addnc  35831  itg2gt0cn  35832  ibladdnclem  35833  iblabsnc  35841  iblmulc2nc  35842  ftc1anclem6  35855  ftc1anclem7  35856  ftc1anclem8  35857  ftc1anc  35858  frinfm  35893  sdclem1  35901  ssbnd  35946  rngoueqz  36098  lssatle  37029  ltrneq2  38162  tendoeq2  38788  lcmineqlem12  40048  hbtlem7  40950  itgoss  40988  trclrelexplem  41319  rfovcnvf1od  41612  dssmapf1od  41629  neik0pk1imk0  41657  collexd  41875  prodeq2ad  43133  0cnv  43283  itgperiod  43522  stoweidlem35  43576  stoweidlem59  43600  fourierdlem31  43679  subsaliuncllem  43896  subsaliuncl  43897  iundjiun  43998  hoiprodcl2  44093  ovnsslelem  44098  ovn0lem  44103  hoidmvlelem3  44135  smflimlem1  44306  smflimlem2  44307  smflimlem3  44308  fundcmpsurinjlem2  44851  sprval  44931  prprval  44966  rmsupp0  45704  lincop  45749  lcoc0  45763