Theorem ralrimivw 3131

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  r19.21v  3160  r19.37v  3161  r19.27v  3164  r19.28v  3166  2rmorex  3697  2reurex  3703  riinrab  5015  exse  5580  mpoeq12  7429  ovmpt3rabdm  7615  offveqb  7647  epweon  7718  exse2  7857  xpexgALT  7923  opabn1stprc  8000  mpoexg  8018  boxriin  8877  fisupg  9187  fisup2g  9371  fisupcl  9372  fiinfg  9403  fiinf2g  9404  ordtypelem8  9429  wemapso2  9457  cantnflem1  9599  r1val1  9699  updjud  9847  dfac12k  10059  compssiso  10285  axcclem  10368  ondomon  10474  tskuni  10695  pinq  10839  supexpr  10966  dedekind  11298  supadd  12113  supmullem2  12116  zsupss  12876  qextlt  13144  qextle  13145  xrsupsslem  13248  xrinfmsslem  13249  supxrpnf  13259  ssnn0fi  13936  recan  15288  climconst  15494  sumeq2sdvOLD  15655  dvdsext  16279  smupvallem  16441  smumullem  16450  pc11  16840  prmreclem4  16879  vdwmc2  16939  vdwlem8  16948  vdwlem13  16953  cshwsex  17060  cshws0  17061  prdsplusg  17410  prdsmulr  17411  prdsvsca  17412  prdshom  17419  imasplusg  17470  imasmulr  17471  imasip  17474  imasaddvallem  17482  imasvscaf  17492  quslem  17496  divsfval  17500  mrcuni  17576  catideu  17630  homfeqd  17650  comfeqd  17662  2oppccomf  17680  catcoppccl  18073  lublecllem  18313  chnfi  18589  pmtrrn  19421  pmtrfrn  19422  gsummptif1n0  19930  ip2eq  21622  frlmup4  21770  evlseu  22050  pmatcollpw2lem  22730  basdif0  22906  clsval2  23003  neif  23053  ordtbaslem  23141  ordtrest2lem  23156  lmconst  23214  cndis  23244  pnrmopn  23296  cmpfi  23361  finptfin  23471  comppfsc  23485  ptbasfi  23534  pttoponconst  23550  ptcnplem  23574  pthaus  23591  xkoptsub  23607  xkopt  23608  nrmr0reg  23702  ordthmeolem  23754  fbssfi  23790  filconn  23836  hausflim  23934  cnpflf  23954  fclscf  23978  cnpfcf  23994  alexsublem  23997  ptcmplem2  24006  ptcmplem3  24007  tsmsfbas  24081  eltsms  24086  utopbas  24188  isucn2  24231  psmetutop  24520  nrginvrcn  24645  lebnumlem3  24918  fmcfil  25227  ovolicc2lem4  25475  mbfconst  25588  i1fmul  25651  itg2const  25695  itg2cnlem2  25717  itgle  25765  ibladdlem  25775  iblabs  25784  iblabsr  25785  iblmulc2  25786  bddmulibl  25794  bddiblnc  25797  ellimc2  25832  limcnlp  25833  c1lip1  25952  itgpowd  26005  ply1nzb  26076  ulm0  26344  itgulm2  26362  dchrhash  27222  lgsquadlem2  27332  2sqlem10  27379  dchrisum  27443  rpvmasum2  27463  pntlemj  27554  bday0b  27793  axcontlem12  29032  nbgr0edg  29414  rusgr1vtx  29645  uspgr2wlkeq2  29703  clwwlknondisj  30169  ip2eqi  30915  ubthlem1  30929  hial2eq  31165  pjnmopi  32207  ssmd1  32370  chrelat2i  32424  xrofsup  32828  prodindf  32910  extdgfialglem2  33825  ordtrest2NEWlem  34054  truae  34375  mbfmcst  34391  mbfmcnt  34400  dya2iocuni  34415  0rrv  34583  hashreprin  34752  reprgt  34753  breprexplemc  34764  breprexp  34765  circlemeth  34772  hgt750lema  34789  fineqvnttrclselem1  35253  fineqvnttrclse  35256  vonf1owev  35278  wevgblacfn  35279  cvmliftlem15  35468  satf0suclem  35545  fmla0disjsuc  35568  fmlasucdisj  35569  neibastop2lem  36530  tailf  36545  filnetlem4  36551  fin2so  37916  matunitlindflem1  37925  matunitlindflem2  37926  poimirlem26  37955  poimirlem28  37957  ismblfin  37970  cnambfre  37977  itg2addnclem  37980  itg2addnc  37983  itg2gt0cn  37984  ibladdnclem  37985  iblabsnc  37993  iblmulc2nc  37994  ftc1anclem6  38007  ftc1anclem7  38008  ftc1anclem8  38009  ftc1anc  38010  frinfm  38044  sdclem1  38052  ssbnd  38097  rngoueqz  38249  lssatle  39449  ltrneq2  40582  tendoeq2  41208  lcmineqlem12  42467  hbtlem7  43541  trclrelexplem  44126  rfovcnvf1od  44419  dssmapf1od  44436  neik0pk1imk0  44462  collexd  44672  sswfaxreg  45402  omssaxinf2  45403  prodeq2ad  46010  0cnv  46158  itgperiod  46397  stoweidlem35  46451  stoweidlem59  46475  fourierdlem31  46554  subsaliuncllem  46773  subsaliuncl  46774  iundjiun  46876  hoiprodcl2  46971  ovn0lem  46981  hoidmvlelem3  47013  smflimlem1  47187  smflimlem2  47188  smflimlem3  47189  fundcmpsurinjlem2  47847  sprval  47927  prprval  47962  rmsupp0  48832  lincop  48872  lcoc0  48886  nelsubclem  49530