Theorem ralrimivw 2967

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

Syntax hints:   → wi 4   ∈ wcel 1990  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  2rmorex  3412  riinrab  4596  exse  5078  dmxp  5344  mpt2eq12  6715  ovmpt3rabdm  6892  offveqb  6919  exse2  7105  xpexgALT  7161  opabn1stprc  7228  mpt2exg  7245  uniqs  7807  boxriin  7950  fisupg  8208  fisup2g  8374  fisupcl  8375  fiinfg  8405  fiinf2g  8406  ordtypelem8  8430  wemapso2  8458  cantnflem1  8586  r1val1  8649  scottex  8748  dfac12k  8969  compssiso  9196  axcclem  9279  ondomon  9385  tskuni  9605  pinq  9749  supexpr  9876  dedekind  10200  supadd  10991  supmullem2  10994  zsupss  11777  qextlt  12034  qextle  12035  xrsupsslem  12137  xrinfmsslem  12138  supxrpnf  12148  ssnn0fi  12784  recan  14076  climconst  14274  sumeq2ad  14434  dvdsext  15043  smupvallem  15205  smumullem  15214  pc11  15584  prmreclem4  15623  vdwmc2  15683  vdwlem8  15692  vdwlem13  15697  cshwsex  15807  cshws0  15808  prdsplusg  16118  prdsmulr  16119  prdsvsca  16120  prdshom  16127  imasplusg  16177  imasmulr  16178  imasip  16181  imasaddvallem  16189  imasvscaf  16199  quslem  16203  divsfval  16207  mrcuni  16281  catideu  16336  homfeqd  16355  comfeqd  16367  2oppccomf  16385  catcoppccl  16758  lublecllem  16988  pmtrrn  17877  pmtrfrn  17878  gsummptif1n0  18365  evlseu  19516  ip2eq  19998  frlmup4  20140  pmatcollpw2lem  20582  basdif0  20757  clsval2  20854  neif  20904  ordtbaslem  20992  ordtrest2lem  21007  lmconst  21065  cndis  21095  pnrmopn  21147  cmpfi  21211  finptfin  21321  comppfsc  21335  ptbasfi  21384  pttoponconst  21400  ptcnplem  21424  pthaus  21441  xkoptsub  21457  xkopt  21458  nrmr0reg  21552  ordthmeolem  21604  fbssfi  21641  filconn  21687  hausflim  21785  cnpflf  21805  fclscf  21829  cnpfcf  21845  alexsublem  21848  ptcmplem2  21857  ptcmplem3  21858  tsmsfbas  21931  eltsms  21936  utopbas  22039  isucn2  22083  psmetutop  22372  nrginvrcn  22496  lebnumlem3  22762  fmcfil  23070  ovolicc2lem4  23288  mbfconst  23402  i1fmul  23463  itg2const  23507  itg2cnlem2  23529  itgle  23576  ibladdlem  23586  iblabs  23595  iblabsr  23596  iblmulc2  23597  bddmulibl  23605  ellimc2  23641  limcnlp  23642  c1lip1  23760  ply1nzb  23882  ulm0  24145  itgulm2  24163  dchrhash  24996  lgsquadlem2  25106  2sqlem10  25153  dchrisum  25181  rpvmasum2  25201  pntlemj  25292  axcontlem12  25855  nbgr0edg  26253  rusgr1vtx  26484  uspgr2wlkeq2  26543  clwwlksndisj  26973  ip2eqi  27712  ubthlem1  27726  hial2eq  27963  occon  28146  spanss  28207  pjnmopi  29007  ssmd1  29170  chrelat2i  29224  xrofsup  29533  ordtrest2NEWlem  29968  prodindf  30085  truae  30306  mbfmcst  30321  mbfmcnt  30330  dya2iocuni  30345  0rrv  30513  hashreprin  30698  reprgt  30699  breprexplemc  30710  breprexp  30711  circlemeth  30718  hgt750lema  30735  cvmliftlem15  31280  trpredss  31729  neibastop2lem  32355  tailf  32370  filnetlem4  32376  fin2so  33396  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem26  33435  poimirlem28  33437  ismblfin  33450  cnambfre  33458  itg2addnclem  33461  itg2addnc  33464  itg2gt0cn  33465  ibladdnclem  33466  iblabsnc  33474  iblmulc2nc  33475  bddiblnc  33480  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  frinfm  33530  sdclem1  33539  ssbnd  33587  rngoueqz  33739  lssatle  34302  ltrneq2  35434  tendoeq2  36062  hbtlem7  37695  itgoss  37733  itgpowd  37800  trclrelexplem  38003  rfovcnvf1od  38298  dssmapf1od  38315  prodeq2ad  39824  0cnv  39974  itgperiod  40197  stoweidlem35  40252  stoweidlem59  40276  fourierdlem31  40355  subsaliuncllem  40575  subsaliuncl  40576  iundjiun  40677  hoiprodcl2  40769  ovnsslelem  40774  ovn0lem  40779  hoidmvlelem3  40811  smflimlem1  40979  smflimlem2  40980  smflimlem3  40981  2reurex  41181  sprval  41729  rmsupp0  42149  lincop  42197  lcoc0  42211