Theorem ralrimivw 3136

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3051

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 3052

This theorem is referenced by:  r19.21v  3165  r19.37v  3167  r19.27v  3173  r19.28v  3175  2rmorex  3737  2reurex  3743  riinrab  5060  exse  5614  dmxpOLD  5909  mpoeq12  7478  ovmpt3rabdm  7664  offveqb  7696  epweon  7767  exse2  7911  xpexgALT  7978  opabn1stprc  8055  mpoexg  8073  uniqs  8789  boxriin  8952  fisupg  9294  fisup2g  9479  fisupcl  9480  fiinfg  9511  fiinf2g  9512  ordtypelem8  9537  wemapso2  9565  cantnflem1  9701  r1val1  9798  updjud  9946  dfac12k  10160  compssiso  10386  axcclem  10469  ondomon  10575  tskuni  10795  pinq  10939  supexpr  11066  dedekind  11396  supadd  12208  supmullem2  12211  zsupss  12951  qextlt  13217  qextle  13218  xrsupsslem  13321  xrinfmsslem  13322  supxrpnf  13332  ssnn0fi  14001  recan  15353  climconst  15557  sumeq2sdvOLD  15718  dvdsext  16338  smupvallem  16500  smumullem  16509  pc11  16898  prmreclem4  16937  vdwmc2  16997  vdwlem8  17006  vdwlem13  17011  cshwsex  17118  cshws0  17119  prdsplusg  17470  prdsmulr  17471  prdsvsca  17472  prdshom  17479  imasplusg  17529  imasmulr  17530  imasip  17533  imasaddvallem  17541  imasvscaf  17551  quslem  17555  divsfval  17559  mrcuni  17631  catideu  17685  homfeqd  17705  comfeqd  17717  2oppccomf  17735  catcoppccl  18128  lublecllem  18368  pmtrrn  19436  pmtrfrn  19437  gsummptif1n0  19945  ip2eq  21611  frlmup4  21759  evlseu  22039  pmatcollpw2lem  22713  basdif0  22889  clsval2  22986  neif  23036  ordtbaslem  23124  ordtrest2lem  23139  lmconst  23197  cndis  23227  pnrmopn  23279  cmpfi  23344  finptfin  23454  comppfsc  23468  ptbasfi  23517  pttoponconst  23533  ptcnplem  23557  pthaus  23574  xkoptsub  23590  xkopt  23591  nrmr0reg  23685  ordthmeolem  23737  fbssfi  23773  filconn  23819  hausflim  23917  cnpflf  23937  fclscf  23961  cnpfcf  23977  alexsublem  23980  ptcmplem2  23989  ptcmplem3  23990  tsmsfbas  24064  eltsms  24069  utopbas  24172  isucn2  24215  psmetutop  24504  nrginvrcn  24629  lebnumlem3  24911  fmcfil  25222  ovolicc2lem4  25471  mbfconst  25584  i1fmul  25647  itg2const  25691  itg2cnlem2  25713  itgle  25761  ibladdlem  25771  iblabs  25780  iblabsr  25781  iblmulc2  25782  bddmulibl  25790  bddiblnc  25793  ellimc2  25828  limcnlp  25829  c1lip1  25952  itgpowd  26007  ply1nzb  26078  ulm0  26350  itgulm2  26368  dchrhash  27232  lgsquadlem2  27342  2sqlem10  27389  dchrisum  27453  rpvmasum2  27473  pntlemj  27564  bday0b  27792  axcontlem12  28900  nbgr0edg  29282  rusgr1vtx  29514  uspgr2wlkeq2  29573  clwwlknondisj  30038  ip2eqi  30783  ubthlem1  30797  hial2eq  31033  pjnmopi  32075  ssmd1  32238  chrelat2i  32292  xrofsup  32690  prodindf  32786  ordtrest2NEWlem  33899  truae  34220  mbfmcst  34237  mbfmcnt  34246  dya2iocuni  34261  0rrv  34429  hashreprin  34598  reprgt  34599  breprexplemc  34610  breprexp  34611  circlemeth  34618  hgt750lema  34635  wevgblacfn  35077  cvmliftlem15  35266  satf0suclem  35343  fmla0disjsuc  35366  fmlasucdisj  35367  neibastop2lem  36324  tailf  36339  filnetlem4  36345  fin2so  37577  matunitlindflem1  37586  matunitlindflem2  37587  poimirlem26  37616  poimirlem28  37618  ismblfin  37631  cnambfre  37638  itg2addnclem  37641  itg2addnc  37644  itg2gt0cn  37645  ibladdnclem  37646  iblabsnc  37654  iblmulc2nc  37655  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  frinfm  37705  sdclem1  37713  ssbnd  37758  rngoueqz  37910  lssatle  38979  ltrneq2  40113  tendoeq2  40739  lcmineqlem12  41999  hbtlem7  43096  trclrelexplem  43682  rfovcnvf1od  43975  dssmapf1od  43992  neik0pk1imk0  44018  collexd  44229  sswfaxreg  44960  omssaxinf2  44961  prodeq2ad  45569  0cnv  45719  itgperiod  45958  stoweidlem35  46012  stoweidlem59  46036  fourierdlem31  46115  subsaliuncllem  46334  subsaliuncl  46335  iundjiun  46437  hoiprodcl2  46532  ovn0lem  46542  hoidmvlelem3  46574  smflimlem1  46748  smflimlem2  46749  smflimlem3  46750  fundcmpsurinjlem2  47361  sprval  47441  prprval  47476  rmsupp0  48291  lincop  48332  lcoc0  48346  nelsubclem  48982