Theorem ralrimivw 3183

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

Syntax hints:   → wi 4   ∈ wcel 2110  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-ral 3143

This theorem is referenced by:  r19.27v  3184  r19.28v  3186  r19.37v  3344  2rmorex  3744  2reurex  3749  riinrab  4998  exse  5513  dmxp  5793  mpoeq12  7221  ovmpt3rabdm  7398  offveqb  7425  exse2  7616  xpexgALT  7676  opabn1stprc  7750  mpoexg  7768  uniqs  8351  boxriin  8498  fisupg  8760  fisup2g  8926  fisupcl  8927  fiinfg  8957  fiinf2g  8958  ordtypelem8  8983  wemapso2  9011  cantnflem1  9146  r1val1  9209  scottex  9308  updjud  9357  dfac12k  9567  compssiso  9790  axcclem  9873  ondomon  9979  tskuni  10199  pinq  10343  supexpr  10470  dedekind  10797  supadd  11603  supmullem2  11606  zsupss  12331  qextlt  12590  qextle  12591  xrsupsslem  12694  xrinfmsslem  12695  supxrpnf  12705  ssnn0fi  13347  recan  14690  climconst  14894  sumeq2sdv  15055  dvdsext  15665  smupvallem  15826  smumullem  15835  pc11  16210  prmreclem4  16249  vdwmc2  16309  vdwlem8  16318  vdwlem13  16323  cshwsex  16428  cshws0  16429  prdsplusg  16725  prdsmulr  16726  prdsvsca  16727  prdshom  16734  imasplusg  16784  imasmulr  16785  imasip  16788  imasaddvallem  16796  imasvscaf  16806  quslem  16810  divsfval  16814  mrcuni  16886  catideu  16940  homfeqd  16959  comfeqd  16971  2oppccomf  16989  catcoppccl  17362  lublecllem  17592  pmtrrn  18579  pmtrfrn  18580  gsummptif1n0  19080  evlseu  20290  ip2eq  20791  frlmup4  20939  pmatcollpw2lem  21379  basdif0  21555  clsval2  21652  neif  21702  ordtbaslem  21790  ordtrest2lem  21805  lmconst  21863  cndis  21893  pnrmopn  21945  cmpfi  22010  finptfin  22120  comppfsc  22134  ptbasfi  22183  pttoponconst  22199  ptcnplem  22223  pthaus  22240  xkoptsub  22256  xkopt  22257  nrmr0reg  22351  ordthmeolem  22403  fbssfi  22439  filconn  22485  hausflim  22583  cnpflf  22603  fclscf  22627  cnpfcf  22643  alexsublem  22646  ptcmplem2  22655  ptcmplem3  22656  tsmsfbas  22730  eltsms  22735  utopbas  22838  isucn2  22882  psmetutop  23171  nrginvrcn  23295  lebnumlem3  23561  fmcfil  23869  ovolicc2lem4  24115  mbfconst  24228  i1fmul  24291  itg2const  24335  itg2cnlem2  24357  itgle  24404  ibladdlem  24414  iblabs  24423  iblabsr  24424  iblmulc2  24425  bddmulibl  24433  ellimc2  24469  limcnlp  24470  c1lip1  24588  ply1nzb  24710  ulm0  24973  itgulm2  24991  dchrhash  25841  lgsquadlem2  25951  2sqlem10  25998  dchrisum  26062  rpvmasum2  26082  pntlemj  26173  axcontlem12  26755  nbgr0edg  27133  rusgr1vtx  27364  uspgr2wlkeq2  27422  clwwlknondisj  27884  ip2eqi  28627  ubthlem1  28641  hial2eq  28877  occon  29058  spanss  29119  pjnmopi  29919  ssmd1  30082  chrelat2i  30136  xrofsup  30486  ordtrest2NEWlem  31160  prodindf  31277  truae  31497  mbfmcst  31512  mbfmcnt  31521  dya2iocuni  31536  0rrv  31704  hashreprin  31886  reprgt  31887  breprexplemc  31898  breprexp  31899  circlemeth  31906  hgt750lema  31923  cvmliftlem15  32540  satf0suclem  32617  fmla0disjsuc  32640  fmlasucdisj  32641  trpredss  33063  neibastop2lem  33703  tailf  33718  filnetlem4  33724  fin2so  34873  matunitlindflem1  34882  matunitlindflem2  34883  poimirlem26  34912  poimirlem28  34914  ismblfin  34927  cnambfre  34934  itg2addnclem  34937  itg2addnc  34940  itg2gt0cn  34941  ibladdnclem  34942  iblabsnc  34950  iblmulc2nc  34951  bddiblnc  34956  ftc1anclem6  34966  ftc1anclem7  34967  ftc1anclem8  34968  ftc1anc  34969  frinfm  35004  sdclem1  35012  ssbnd  35060  rngoueqz  35212  lssatle  36145  ltrneq2  37278  tendoeq2  37904  hbtlem7  39718  itgoss  39756  itgpowd  39814  trclrelexplem  40049  rfovcnvf1od  40343  dssmapf1od  40360  neik0pk1imk0  40390  collexd  40586  prodeq2ad  41866  0cnv  42016  itgperiod  42259  stoweidlem35  42314  stoweidlem59  42338  fourierdlem31  42417  subsaliuncllem  42634  subsaliuncl  42635  iundjiun  42736  hoiprodcl2  42831  ovnsslelem  42836  ovn0lem  42841  hoidmvlelem3  42873  smflimlem1  43041  smflimlem2  43042  smflimlem3  43043  fundcmpsurinjlem2  43553  sprval  43635  prprval  43670  rmsupp0  44410  lincop  44457  lcoc0  44471