Theorem ralrimivw 3162

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

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

This theorem is used by:  r19.21v  3191  r19.37v  3192  r19.27v  3195  r19.28v  3197  2rmorex  3715  2reurex  3721  riinrab  5047  exse  5615  mpoeq12  7513  ovmpt3rabdm  7701  offveqb  7741  epweon  7810  exse2  7950  xpexgALT  8014  opabn1stprc  8091  mpoexg  8111  boxriin  8993  fisupg  9304  fisup2g  9485  fisupcl  9486  fiinfg  9517  fiinf2g  9518  ordtypelem8  9543  wemapso2  9571  cantnflem1  9714  r1val1  9817  updjud  10039  dfac12k  10250  compssiso  10476  axcclem  10559  ondomon  10671  tskuni  10892  pinq  11036  supexpr  11163  dedekind  11497  supadd  12309  supmullem2  12312  zsupss  13088  qextlt  13357  qextle  13358  xrsupsslem  13461  xrinfmsslem  13462  supxrpnf  13472  ssnn0fi  14152  recan  15530  climconst  15736  dvdsext  16517  smupvallem  16679  smumullem  16688  pc11  17084  prmreclem4  17123  vdwmc2  17183  vdwlem8  17192  vdwlem13  17197  cshwsex  17304  cshws0  17305  prdsplusg  17655  prdsmulr  17656  prdsvsca  17657  prdshom  17664  imasplusg  17715  imasmulr  17716  imasip  17719  imasaddvallem  17727  imasvscaf  17737  quslem  17741  divsfval  17745  mrcuni  17821  catideu  17875  homfeqd  17895  comfeqd  17907  2oppccomf  17925  catcoppccl  18318  lublecllem  18558  chnfi  18834  pmtrrn  19698  pmtrfrn  19699  gsummptif1n0  20207  ip2eq  21986  frlmup4  22134  evlseu  22419  matunitlindflem1  23021  matunitlindflem2  23022  pmatcollpw2lem  23122  basdif0  23298  clsval2  23395  neif  23445  ordtbaslem  23533  ordtrest2lem  23548  lmconst  23606  cndis  23636  pnrmopn  23688  cmpfi  23753  finptfin  23864  comppfsc  23878  ptbasfi  23927  pttoponconst  23943  ptcnplem  23967  pthaus  23984  xkoptsub  24000  xkopt  24001  nrmr0reg  24095  ordthmeolem  24147  fbssfi  24183  filconn  24229  hausflim  24327  cnpflf  24347  fclscf  24371  cnpfcf  24387  alexsublem  24390  ptcmplem2  24399  ptcmplem3  24400  tsmsfbas  24474  eltsms  24479  utopbas  24581  isucn2  24624  psmetutop  24913  nrginvrcn  25038  lebnumlem3  25311  fmcfil  25620  ovolicc2lem4  25868  mbfconst  25981  i1fmul  26044  itg2const  26088  itg2cnlem2  26110  itgle  26157  ibladdlem  26167  iblabs  26176  iblabsr  26177  iblmulc2  26178  bddmulibl  26186  bddiblnc  26189  ellimc2  26224  limcnlp  26225  c1lip1  26344  itgpowd  26397  ply1nzb  26468  ulm0  26745  itgulm2  26763  dchrhash  27625  lgsquadlem2  27735  2sqlem10  27782  dchrisum  27846  rpvmasum2  27866  pntlemj  27957  bday0b  28226  axcontlem12  29580  nbgr0edg  29965  rusgr1vtx  30196  uspgr2wlkeq2  30254  clwwlknondisj  30729  ip2eqi  31485  ubthlem1  31499  hial2eq  31735  pjnmopi  32777  ssmd1  32940  chrelat2i  32994  xrofsup  33426  prodindf  33496  selvply1rhmlemb  34218  extdgfialglem2  34392  ordtrest2NEWlem  34621  truae  34943  mbfmcst  34958  mbfmcnt  34967  dya2iocuni  34982  0rrv  35150  hashreprin  35316  reprgt  35317  breprexplemc  35328  breprexp  35329  circlemeth  35336  hgt750lema  35353  0elscott  35836  fineqvnttrclselem1  35888  fineqvnttrclse  35891  vonf1wev  36035  vonf1owevOLD  36037  wevgblacfn  36038  wevsev  36040  onvfowev  36049  cvmliftlem15  36229  satf0suclem  36306  fmla0disjsuc  36329  fmlasucdisj  36330  mirimanoffr  36626  neibastop2lem  37325  tailf  37340  filnetlem4  37346  fin2so  38721  poimirlem26  38755  poimirlem28  38757  ismblfin  38770  cnambfre  38777  itg2addnclem  38780  itg2addnc  38783  itg2gt0cn  38784  ibladdnclem  38785  iblabsnc  38793  iblmulc2nc  38794  ftc1anclem6  38807  ftc1anclem7  38808  ftc1anclem8  38809  ftc1anc  38810  frinfm  38860  sdclem1  38868  ssbnd  38913  rngoueqz  39065  lssatle  40263  ltrneq2  41396  tendoeq2  42022  lcmineqlem12  43281  hbtlem7  44317  trclrelexplem  44901  rfovcnvf1od  45194  dssmapf1od  45211  neik0pk1imk0  45237  collexd  45431  sswfaxreg  46170  omssaxinf2  46171  prodeq2ad  46807  0cnv  46955  itgperiod  47194  stoweidlem35  47248  stoweidlem59  47272  fourierdlem31  47351  subsaliuncllem  47570  subsaliuncl  47571  iundjiun  47673  hoiprodcl2  47768  ovn0lem  47778  hoidmvlelem3  47810  smflimlem1  47984  smflimlem2  47985  smflimlem3  47986  tmachlem-tpbase  48152  tmachlem-extpcover  48158  tmachlem-agreefin  48161  fundcmpsurinjlem2  48684  sprval  48764  prprval  48799  rmsupp0  49683  lincop  49723  lcoc0  49737  nelsubclem  50384