Theorem ralrimivw 3139

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

Syntax hints:   → wi 4   ∈ wcel 2098  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-ral 3051

This theorem is referenced by:  r19.21v  3169  r19.37v  3171  r19.27v  3177  r19.28v  3179  2rmorex  3746  2reurex  3752  riinrab  5088  exse  5641  dmxp  5931  mpoeq12  7493  ovmpt3rabdm  7680  offveqb  7711  epweon  7778  exse2  7925  xpexgALT  7986  opabn1stprc  8063  mpoexg  8081  uniqs  8796  boxriin  8959  fisupg  9316  fisup2g  9493  fisupcl  9494  fiinfg  9524  fiinf2g  9525  ordtypelem8  9550  wemapso2  9578  cantnflem1  9714  r1val1  9811  updjud  9959  dfac12k  10172  compssiso  10399  axcclem  10482  ondomon  10588  tskuni  10808  pinq  10952  supexpr  11079  dedekind  11409  supadd  12215  supmullem2  12218  zsupss  12954  qextlt  13217  qextle  13218  xrsupsslem  13321  xrinfmsslem  13322  supxrpnf  13332  ssnn0fi  13986  recan  15319  climconst  15523  sumeq2sdv  15686  dvdsext  16301  smupvallem  16461  smumullem  16470  pc11  16852  prmreclem4  16891  vdwmc2  16951  vdwlem8  16960  vdwlem13  16965  cshwsex  17073  cshws0  17074  prdsplusg  17443  prdsmulr  17444  prdsvsca  17445  prdshom  17452  imasplusg  17502  imasmulr  17503  imasip  17506  imasaddvallem  17514  imasvscaf  17524  quslem  17528  divsfval  17532  mrcuni  17604  catideu  17658  homfeqd  17678  comfeqd  17690  2oppccomf  17710  catcoppccl  18109  catcoppcclOLD  18110  lublecllem  18355  pmtrrn  19424  pmtrfrn  19425  gsummptif1n0  19933  ip2eq  21602  frlmup4  21752  evlseu  22051  pmatcollpw2lem  22723  basdif0  22900  clsval2  22998  neif  23048  ordtbaslem  23136  ordtrest2lem  23151  lmconst  23209  cndis  23239  pnrmopn  23291  cmpfi  23356  finptfin  23466  comppfsc  23480  ptbasfi  23529  pttoponconst  23545  ptcnplem  23569  pthaus  23586  xkoptsub  23602  xkopt  23603  nrmr0reg  23697  ordthmeolem  23749  fbssfi  23785  filconn  23831  hausflim  23929  cnpflf  23949  fclscf  23973  cnpfcf  23989  alexsublem  23992  ptcmplem2  24001  ptcmplem3  24002  tsmsfbas  24076  eltsms  24081  utopbas  24184  isucn2  24228  psmetutop  24520  nrginvrcn  24653  lebnumlem3  24933  fmcfil  25244  ovolicc2lem4  25493  mbfconst  25606  i1fmul  25669  itg2const  25714  itg2cnlem2  25736  itgle  25783  ibladdlem  25793  iblabs  25802  iblabsr  25803  iblmulc2  25804  bddmulibl  25812  bddiblnc  25815  ellimc2  25850  limcnlp  25851  c1lip1  25974  itgpowd  26029  ply1nzb  26103  ulm0  26372  itgulm2  26390  dchrhash  27249  lgsquadlem2  27359  2sqlem10  27406  dchrisum  27470  rpvmasum2  27490  pntlemj  27581  bday0b  27809  axcontlem12  28858  nbgr0edg  29242  rusgr1vtx  29474  uspgr2wlkeq2  29533  clwwlknondisj  29993  ip2eqi  30738  ubthlem1  30752  hial2eq  30988  pjnmopi  32030  ssmd1  32193  chrelat2i  32247  xrofsup  32619  ordtrest2NEWlem  33654  prodindf  33773  truae  33993  mbfmcst  34010  mbfmcnt  34019  dya2iocuni  34034  0rrv  34202  hashreprin  34383  reprgt  34384  breprexplemc  34395  breprexp  34396  circlemeth  34403  hgt750lema  34420  cvmliftlem15  35039  satf0suclem  35116  fmla0disjsuc  35139  fmlasucdisj  35140  neibastop2lem  35975  tailf  35990  filnetlem4  35996  fin2so  37211  matunitlindflem1  37220  matunitlindflem2  37221  poimirlem26  37250  poimirlem28  37252  ismblfin  37265  cnambfre  37272  itg2addnclem  37275  itg2addnc  37278  itg2gt0cn  37279  ibladdnclem  37280  iblabsnc  37288  iblmulc2nc  37289  ftc1anclem6  37302  ftc1anclem7  37303  ftc1anclem8  37304  ftc1anc  37305  frinfm  37339  sdclem1  37347  ssbnd  37392  rngoueqz  37544  lssatle  38617  ltrneq2  39751  tendoeq2  40377  lcmineqlem12  41643  hbtlem7  42691  trclrelexplem  43283  rfovcnvf1od  43576  dssmapf1od  43593  neik0pk1imk0  43619  collexd  43836  prodeq2ad  45118  0cnv  45268  itgperiod  45507  stoweidlem35  45561  stoweidlem59  45585  fourierdlem31  45664  subsaliuncllem  45883  subsaliuncl  45884  iundjiun  45986  hoiprodcl2  46081  ovn0lem  46091  hoidmvlelem3  46123  smflimlem1  46297  smflimlem2  46298  smflimlem3  46299  fundcmpsurinjlem2  46876  sprval  46956  prprval  46991  rmsupp0  47618  lincop  47662  lcoc0  47676