Theorem ralrimivw 3129

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ral 3045

This theorem is referenced by:  r19.21v  3158  r19.37v  3160  r19.27v  3166  r19.28v  3168  2rmorex  3725  2reurex  3731  riinrab  5048  exse  5598  dmxpOLD  5893  mpoeq12  7462  ovmpt3rabdm  7648  offveqb  7680  epweon  7751  exse2  7893  xpexgALT  7960  opabn1stprc  8037  mpoexg  8055  boxriin  8913  fisupg  9235  fisup2g  9420  fisupcl  9421  fiinfg  9452  fiinf2g  9453  ordtypelem8  9478  wemapso2  9506  cantnflem1  9642  r1val1  9739  updjud  9887  dfac12k  10101  compssiso  10327  axcclem  10410  ondomon  10516  tskuni  10736  pinq  10880  supexpr  11007  dedekind  11337  supadd  12151  supmullem2  12154  zsupss  12896  qextlt  13163  qextle  13164  xrsupsslem  13267  xrinfmsslem  13268  supxrpnf  13278  ssnn0fi  13950  recan  15303  climconst  15509  sumeq2sdvOLD  15670  dvdsext  16291  smupvallem  16453  smumullem  16462  pc11  16851  prmreclem4  16890  vdwmc2  16950  vdwlem8  16959  vdwlem13  16964  cshwsex  17071  cshws0  17072  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdshom  17430  imasplusg  17480  imasmulr  17481  imasip  17484  imasaddvallem  17492  imasvscaf  17502  quslem  17506  divsfval  17510  mrcuni  17582  catideu  17636  homfeqd  17656  comfeqd  17668  2oppccomf  17686  catcoppccl  18079  lublecllem  18319  pmtrrn  19387  pmtrfrn  19388  gsummptif1n0  19896  ip2eq  21562  frlmup4  21710  evlseu  21990  pmatcollpw2lem  22664  basdif0  22840  clsval2  22937  neif  22987  ordtbaslem  23075  ordtrest2lem  23090  lmconst  23148  cndis  23178  pnrmopn  23230  cmpfi  23295  finptfin  23405  comppfsc  23419  ptbasfi  23468  pttoponconst  23484  ptcnplem  23508  pthaus  23525  xkoptsub  23541  xkopt  23542  nrmr0reg  23636  ordthmeolem  23688  fbssfi  23724  filconn  23770  hausflim  23868  cnpflf  23888  fclscf  23912  cnpfcf  23928  alexsublem  23931  ptcmplem2  23940  ptcmplem3  23941  tsmsfbas  24015  eltsms  24020  utopbas  24123  isucn2  24166  psmetutop  24455  nrginvrcn  24580  lebnumlem3  24862  fmcfil  25172  ovolicc2lem4  25421  mbfconst  25534  i1fmul  25597  itg2const  25641  itg2cnlem2  25663  itgle  25711  ibladdlem  25721  iblabs  25730  iblabsr  25731  iblmulc2  25732  bddmulibl  25740  bddiblnc  25743  ellimc2  25778  limcnlp  25779  c1lip1  25902  itgpowd  25957  ply1nzb  26028  ulm0  26300  itgulm2  26318  dchrhash  27182  lgsquadlem2  27292  2sqlem10  27339  dchrisum  27403  rpvmasum2  27423  pntlemj  27514  bday0b  27742  axcontlem12  28902  nbgr0edg  29284  rusgr1vtx  29516  uspgr2wlkeq2  29575  clwwlknondisj  30040  ip2eqi  30785  ubthlem1  30799  hial2eq  31035  pjnmopi  32077  ssmd1  32240  chrelat2i  32294  xrofsup  32690  prodindf  32786  ordtrest2NEWlem  33912  truae  34233  mbfmcst  34250  mbfmcnt  34259  dya2iocuni  34274  0rrv  34442  hashreprin  34611  reprgt  34612  breprexplemc  34623  breprexp  34624  circlemeth  34631  hgt750lema  34648  vonf1owev  35095  wevgblacfn  35096  cvmliftlem15  35285  satf0suclem  35362  fmla0disjsuc  35385  fmlasucdisj  35386  neibastop2lem  36348  tailf  36363  filnetlem4  36369  fin2so  37601  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem26  37640  poimirlem28  37642  ismblfin  37655  cnambfre  37662  itg2addnclem  37665  itg2addnc  37668  itg2gt0cn  37669  ibladdnclem  37670  iblabsnc  37678  iblmulc2nc  37679  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  frinfm  37729  sdclem1  37737  ssbnd  37782  rngoueqz  37934  lssatle  39008  ltrneq2  40142  tendoeq2  40768  lcmineqlem12  42028  hbtlem7  43114  trclrelexplem  43700  rfovcnvf1od  43993  dssmapf1od  44010  neik0pk1imk0  44036  collexd  44246  sswfaxreg  44977  omssaxinf2  44978  prodeq2ad  45590  0cnv  45740  itgperiod  45979  stoweidlem35  46033  stoweidlem59  46057  fourierdlem31  46136  subsaliuncllem  46355  subsaliuncl  46356  iundjiun  46458  hoiprodcl2  46553  ovn0lem  46563  hoidmvlelem3  46595  smflimlem1  46769  smflimlem2  46770  smflimlem3  46771  fundcmpsurinjlem2  47400  sprval  47480  prprval  47515  rmsupp0  48356  lincop  48397  lcoc0  48411  nelsubclem  49056