Theorem ralrimivw 3158

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 26	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralrimiv 3153	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-ral 3077

This theorem is used by:  r19.21v  3187  r19.37v  3188  r19.27v  3191  r19.28v  3193  2rmorex  3711  2reurex  3717  riinrab  5043  exse  5610  mpoeq12  7493  ovmpt3rabdm  7680  offveqb  7720  epweon  7789  exse2  7929  xpexgALT  7993  opabn1stprc  8069  mpoexg  8089  boxriin  8968  fisupg  9279  fisup2g  9461  fisupcl  9462  fiinfg  9493  fiinf2g  9494  ordtypelem8  9519  wemapso2  9547  cantnflem1  9690  r1val1  9793  updjud  10015  dfac12k  10226  compssiso  10452  axcclem  10535  ondomon  10647  tskuni  10868  pinq  11012  supexpr  11139  dedekind  11473  supadd  12285  supmullem2  12288  zsupss  13064  qextlt  13333  qextle  13334  xrsupsslem  13437  xrinfmsslem  13438  supxrpnf  13448  ssnn0fi  14128  recan  15504  climconst  15710  dvdsext  16491  smupvallem  16653  smumullem  16662  pc11  17058  prmreclem4  17097  vdwmc2  17157  vdwlem8  17166  vdwlem13  17171  cshwsex  17278  cshws0  17279  prdsplusg  17629  prdsmulr  17630  prdsvsca  17631  prdshom  17638  imasplusg  17689  imasmulr  17690  imasip  17693  imasaddvallem  17701  imasvscaf  17711  quslem  17715  divsfval  17719  mrcuni  17795  catideu  17849  homfeqd  17869  comfeqd  17881  2oppccomf  17899  catcoppccl  18292  lublecllem  18532  chnfi  18808  pmtrrn  19671  pmtrfrn  19672  gsummptif1n0  20180  ip2eq  21959  frlmup4  22107  evlseu  22392  matunitlindflem1  22994  matunitlindflem2  22995  pmatcollpw2lem  23095  basdif0  23271  clsval2  23368  neif  23418  ordtbaslem  23506  ordtrest2lem  23521  lmconst  23579  cndis  23609  pnrmopn  23661  cmpfi  23726  finptfin  23837  comppfsc  23851  ptbasfi  23900  pttoponconst  23916  ptcnplem  23940  pthaus  23957  xkoptsub  23973  xkopt  23974  nrmr0reg  24068  ordthmeolem  24120  fbssfi  24156  filconn  24202  hausflim  24300  cnpflf  24320  fclscf  24344  cnpfcf  24360  alexsublem  24363  ptcmplem2  24372  ptcmplem3  24373  tsmsfbas  24447  eltsms  24452  utopbas  24554  isucn2  24597  psmetutop  24886  nrginvrcn  25011  lebnumlem3  25284  fmcfil  25593  ovolicc2lem4  25841  mbfconst  25954  i1fmul  26017  itg2const  26061  itg2cnlem2  26083  itgle  26130  ibladdlem  26140  iblabs  26149  iblabsr  26150  iblmulc2  26151  bddmulibl  26159  bddiblnc  26162  ellimc2  26197  limcnlp  26198  c1lip1  26317  itgpowd  26370  ply1nzb  26441  ulm0  26718  itgulm2  26736  dchrhash  27598  lgsquadlem2  27708  2sqlem10  27755  dchrisum  27819  rpvmasum2  27839  pntlemj  27930  bday0b  28199  axcontlem12  29553  nbgr0edg  29938  rusgr1vtx  30169  uspgr2wlkeq2  30227  clwwlknondisj  30702  ip2eqi  31458  ubthlem1  31472  hial2eq  31708  pjnmopi  32750  ssmd1  32913  chrelat2i  32967  xrofsup  33359  prodindf  33429  selvply1rhmlemb  34151  extdgfialglem2  34325  ordtrest2NEWlem  34554  truae  34876  mbfmcst  34891  mbfmcnt  34900  dya2iocuni  34915  0rrv  35083  hashreprin  35249  reprgt  35250  breprexplemc  35261  breprexp  35262  circlemeth  35269  hgt750lema  35286  fineqvnttrclselem1  35789  fineqvnttrclse  35792  vonf1wev  35887  vonf1owevOLD  35889  wevgblacfn  35890  onvfowev  35899  cvmliftlem15  36063  satf0suclem  36140  fmla0disjsuc  36163  fmlasucdisj  36164  neibastop2lem  37148  tailf  37163  filnetlem4  37169  fin2so  38531  poimirlem26  38565  poimirlem28  38567  ismblfin  38580  cnambfre  38587  itg2addnclem  38590  itg2addnc  38593  itg2gt0cn  38594  ibladdnclem  38595  iblabsnc  38603  iblmulc2nc  38604  ftc1anclem6  38617  ftc1anclem7  38618  ftc1anclem8  38619  ftc1anc  38620  frinfm  38670  sdclem1  38678  ssbnd  38723  rngoueqz  38875  lssatle  40073  ltrneq2  41206  tendoeq2  41832  lcmineqlem12  43091  hbtlem7  44127  trclrelexplem  44711  rfovcnvf1od  45004  dssmapf1od  45021  neik0pk1imk0  45047  collexd  45241  sswfaxreg  45977  omssaxinf2  45978  prodeq2ad  46604  0cnv  46752  itgperiod  46991  stoweidlem35  47045  stoweidlem59  47069  fourierdlem31  47148  subsaliuncllem  47367  subsaliuncl  47368  iundjiun  47470  hoiprodcl2  47565  ovn0lem  47575  hoidmvlelem3  47607  smflimlem1  47781  smflimlem2  47782  smflimlem3  47783  tmachlem-tpbase  47949  tmachlem-extpcover  47955  tmachlem-agreefin  47958  fundcmpsurinjlem2  48481  sprval  48561  prprval  48596  rmsupp0  49480  lincop  49520  lcoc0  49534  nelsubclem  50175