Theorem ralrimivw 3156

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  r19.21v  3186  r19.37v  3188  r19.27v  3194  r19.28v  3196  2rmorex  3776  2reurex  3782  riinrab  5107  exse  5660  dmxpOLD  5954  mpoeq12  7523  ovmpt3rabdm  7709  offveqb  7740  epweon  7810  exse2  7957  xpexgALT  8022  opabn1stprc  8099  mpoexg  8117  uniqs  8835  boxriin  8998  fisupg  9352  fisup2g  9537  fisupcl  9538  fiinfg  9568  fiinf2g  9569  ordtypelem8  9594  wemapso2  9622  cantnflem1  9758  r1val1  9855  updjud  10003  dfac12k  10217  compssiso  10443  axcclem  10526  ondomon  10632  tskuni  10852  pinq  10996  supexpr  11123  dedekind  11453  supadd  12263  supmullem2  12266  zsupss  13002  qextlt  13265  qextle  13266  xrsupsslem  13369  xrinfmsslem  13370  supxrpnf  13380  ssnn0fi  14036  recan  15385  climconst  15589  sumeq2sdvOLD  15752  dvdsext  16369  smupvallem  16529  smumullem  16538  pc11  16927  prmreclem4  16966  vdwmc2  17026  vdwlem8  17035  vdwlem13  17040  cshwsex  17148  cshws0  17149  prdsplusg  17518  prdsmulr  17519  prdsvsca  17520  prdshom  17527  imasplusg  17577  imasmulr  17578  imasip  17581  imasaddvallem  17589  imasvscaf  17599  quslem  17603  divsfval  17607  mrcuni  17679  catideu  17733  homfeqd  17753  comfeqd  17765  2oppccomf  17785  catcoppccl  18184  catcoppcclOLD  18185  lublecllem  18430  pmtrrn  19499  pmtrfrn  19500  gsummptif1n0  20008  ip2eq  21694  frlmup4  21844  evlseu  22130  pmatcollpw2lem  22804  basdif0  22981  clsval2  23079  neif  23129  ordtbaslem  23217  ordtrest2lem  23232  lmconst  23290  cndis  23320  pnrmopn  23372  cmpfi  23437  finptfin  23547  comppfsc  23561  ptbasfi  23610  pttoponconst  23626  ptcnplem  23650  pthaus  23667  xkoptsub  23683  xkopt  23684  nrmr0reg  23778  ordthmeolem  23830  fbssfi  23866  filconn  23912  hausflim  24010  cnpflf  24030  fclscf  24054  cnpfcf  24070  alexsublem  24073  ptcmplem2  24082  ptcmplem3  24083  tsmsfbas  24157  eltsms  24162  utopbas  24265  isucn2  24309  psmetutop  24601  nrginvrcn  24734  lebnumlem3  25014  fmcfil  25325  ovolicc2lem4  25574  mbfconst  25687  i1fmul  25750  itg2const  25795  itg2cnlem2  25817  itgle  25865  ibladdlem  25875  iblabs  25884  iblabsr  25885  iblmulc2  25886  bddmulibl  25894  bddiblnc  25897  ellimc2  25932  limcnlp  25933  c1lip1  26056  itgpowd  26111  ply1nzb  26182  ulm0  26452  itgulm2  26470  dchrhash  27333  lgsquadlem2  27443  2sqlem10  27490  dchrisum  27554  rpvmasum2  27574  pntlemj  27665  bday0b  27893  axcontlem12  29008  nbgr0edg  29392  rusgr1vtx  29624  uspgr2wlkeq2  29683  clwwlknondisj  30143  ip2eqi  30888  ubthlem1  30902  hial2eq  31138  pjnmopi  32180  ssmd1  32343  chrelat2i  32397  xrofsup  32774  ordtrest2NEWlem  33868  prodindf  33987  truae  34207  mbfmcst  34224  mbfmcnt  34233  dya2iocuni  34248  0rrv  34416  hashreprin  34597  reprgt  34598  breprexplemc  34609  breprexp  34610  circlemeth  34617  hgt750lema  34634  wevgblacfn  35076  cvmliftlem15  35266  satf0suclem  35343  fmla0disjsuc  35366  fmlasucdisj  35367  neibastop2lem  36326  tailf  36341  filnetlem4  36347  fin2so  37567  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem26  37606  poimirlem28  37608  ismblfin  37621  cnambfre  37628  itg2addnclem  37631  itg2addnc  37634  itg2gt0cn  37635  ibladdnclem  37636  iblabsnc  37644  iblmulc2nc  37645  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  frinfm  37695  sdclem1  37703  ssbnd  37748  rngoueqz  37900  lssatle  38971  ltrneq2  40105  tendoeq2  40731  lcmineqlem12  41997  hbtlem7  43082  trclrelexplem  43673  rfovcnvf1od  43966  dssmapf1od  43983  neik0pk1imk0  44009  collexd  44226  prodeq2ad  45513  0cnv  45663  itgperiod  45902  stoweidlem35  45956  stoweidlem59  45980  fourierdlem31  46059  subsaliuncllem  46278  subsaliuncl  46279  iundjiun  46381  hoiprodcl2  46476  ovn0lem  46486  hoidmvlelem3  46518  smflimlem1  46692  smflimlem2  46693  smflimlem3  46694  fundcmpsurinjlem2  47273  sprval  47353  prprval  47388  rmsupp0  48093  lincop  48137  lcoc0  48151