Theorem ralrimivw 3134

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  r19.21v  3163  r19.37v  3164  r19.27v  3167  r19.28v  3169  2rmorex  3701  2reurex  3707  riinrab  5027  exse  5582  mpoeq12  7431  ovmpt3rabdm  7617  offveqb  7649  epweon  7720  exse2  7859  xpexgALT  7925  opabn1stprc  8002  mpoexg  8020  boxriin  8879  fisupg  9189  fisup2g  9373  fisupcl  9374  fiinfg  9405  fiinf2g  9406  ordtypelem8  9431  wemapso2  9459  cantnflem1  9599  r1val1  9699  updjud  9847  dfac12k  10059  compssiso  10285  axcclem  10368  ondomon  10474  tskuni  10695  pinq  10839  supexpr  10966  dedekind  11298  supadd  12113  supmullem2  12116  zsupss  12876  qextlt  13144  qextle  13145  xrsupsslem  13248  xrinfmsslem  13249  supxrpnf  13259  ssnn0fi  13936  recan  15288  climconst  15494  sumeq2sdvOLD  15655  dvdsext  16279  smupvallem  16441  smumullem  16450  pc11  16840  prmreclem4  16879  vdwmc2  16939  vdwlem8  16948  vdwlem13  16953  cshwsex  17060  cshws0  17061  prdsplusg  17410  prdsmulr  17411  prdsvsca  17412  prdshom  17419  imasplusg  17470  imasmulr  17471  imasip  17474  imasaddvallem  17482  imasvscaf  17492  quslem  17496  divsfval  17500  mrcuni  17576  catideu  17630  homfeqd  17650  comfeqd  17662  2oppccomf  17680  catcoppccl  18073  lublecllem  18313  chnfi  18589  pmtrrn  19421  pmtrfrn  19422  gsummptif1n0  19930  ip2eq  21641  frlmup4  21789  evlseu  22070  pmatcollpw2lem  22751  basdif0  22927  clsval2  23024  neif  23074  ordtbaslem  23162  ordtrest2lem  23177  lmconst  23235  cndis  23265  pnrmopn  23317  cmpfi  23382  finptfin  23492  comppfsc  23506  ptbasfi  23555  pttoponconst  23571  ptcnplem  23595  pthaus  23612  xkoptsub  23628  xkopt  23629  nrmr0reg  23723  ordthmeolem  23775  fbssfi  23811  filconn  23857  hausflim  23955  cnpflf  23975  fclscf  23999  cnpfcf  24015  alexsublem  24018  ptcmplem2  24027  ptcmplem3  24028  tsmsfbas  24102  eltsms  24107  utopbas  24209  isucn2  24252  psmetutop  24541  nrginvrcn  24666  lebnumlem3  24939  fmcfil  25248  ovolicc2lem4  25496  mbfconst  25609  i1fmul  25672  itg2const  25716  itg2cnlem2  25738  itgle  25786  ibladdlem  25796  iblabs  25805  iblabsr  25806  iblmulc2  25807  bddmulibl  25815  bddiblnc  25818  ellimc2  25853  limcnlp  25854  c1lip1  25974  itgpowd  26029  ply1nzb  26100  ulm0  26371  itgulm2  26389  dchrhash  27253  lgsquadlem2  27363  2sqlem10  27410  dchrisum  27474  rpvmasum2  27494  pntlemj  27585  bday0b  27824  axcontlem12  29063  nbgr0edg  29445  rusgr1vtx  29677  uspgr2wlkeq2  29735  clwwlknondisj  30201  ip2eqi  30947  ubthlem1  30961  hial2eq  31197  pjnmopi  32239  ssmd1  32402  chrelat2i  32456  xrofsup  32860  prodindf  32942  extdgfialglem2  33858  ordtrest2NEWlem  34087  truae  34408  mbfmcst  34424  mbfmcnt  34433  dya2iocuni  34448  0rrv  34616  hashreprin  34785  reprgt  34786  breprexplemc  34797  breprexp  34798  circlemeth  34805  hgt750lema  34822  fineqvnttrclselem1  35286  fineqvnttrclse  35289  vonf1owev  35311  wevgblacfn  35312  cvmliftlem15  35501  satf0suclem  35578  fmla0disjsuc  35601  fmlasucdisj  35602  neibastop2lem  36563  tailf  36578  filnetlem4  36584  fin2so  37939  matunitlindflem1  37948  matunitlindflem2  37949  poimirlem26  37978  poimirlem28  37980  ismblfin  37993  cnambfre  38000  itg2addnclem  38003  itg2addnc  38006  itg2gt0cn  38007  ibladdnclem  38008  iblabsnc  38016  iblmulc2nc  38017  ftc1anclem6  38030  ftc1anclem7  38031  ftc1anclem8  38032  ftc1anc  38033  frinfm  38067  sdclem1  38075  ssbnd  38120  rngoueqz  38272  lssatle  39472  ltrneq2  40605  tendoeq2  41231  lcmineqlem12  42490  hbtlem7  43568  trclrelexplem  44153  rfovcnvf1od  44446  dssmapf1od  44463  neik0pk1imk0  44489  collexd  44699  sswfaxreg  45429  omssaxinf2  45430  prodeq2ad  46037  0cnv  46185  itgperiod  46424  stoweidlem35  46478  stoweidlem59  46502  fourierdlem31  46581  subsaliuncllem  46800  subsaliuncl  46801  iundjiun  46903  hoiprodcl2  46998  ovn0lem  47008  hoidmvlelem3  47040  smflimlem1  47214  smflimlem2  47215  smflimlem3  47216  fundcmpsurinjlem2  47856  sprval  47936  prprval  47971  rmsupp0  48841  lincop  48881  lcoc0  48895  nelsubclem  49539