Theorem ralrimivw 3158

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 26	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralrimiv 3153	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ral 3077

This theorem is used by:  r19.21v  3187  r19.37v  3188  r19.27v  3191  r19.28v  3193  2rmorex  3712  2reurex  3718  riinrab  5044  exse  5615  mpoeq12  7486  ovmpt3rabdm  7673  offveqb  7705  epweon  7774  exse2  7914  xpexgALT  7978  opabn1stprc  8055  mpoexg  8075  boxriin  8947  fisupg  9258  fisup2g  9439  fisupcl  9440  fiinfg  9471  fiinf2g  9472  ordtypelem8  9497  wemapso2  9525  cantnflem1  9668  r1val1  9768  updjud  9939  dfac12k  10150  compssiso  10376  axcclem  10459  ondomon  10571  tskuni  10792  pinq  10936  supexpr  11063  dedekind  11397  supadd  12207  supmullem2  12210  zsupss  12986  qextlt  13255  qextle  13256  xrsupsslem  13359  xrinfmsslem  13360  supxrpnf  13370  ssnn0fi  14049  recan  15424  climconst  15630  dvdsext  16411  smupvallem  16573  smumullem  16582  pc11  16972  prmreclem4  17011  vdwmc2  17071  vdwlem8  17080  vdwlem13  17085  cshwsex  17192  cshws0  17193  prdsplusg  17543  prdsmulr  17544  prdsvsca  17545  prdshom  17552  imasplusg  17603  imasmulr  17604  imasip  17607  imasaddvallem  17615  imasvscaf  17625  quslem  17629  divsfval  17633  mrcuni  17709  catideu  17763  homfeqd  17783  comfeqd  17795  2oppccomf  17813  catcoppccl  18206  lublecllem  18446  chnfi  18722  pmtrrn  19584  pmtrfrn  19585  gsummptif1n0  20093  ip2eq  21866  frlmup4  22014  evlseu  22299  matunitlindflem1  22901  matunitlindflem2  22902  pmatcollpw2lem  23002  basdif0  23178  clsval2  23275  neif  23325  ordtbaslem  23413  ordtrest2lem  23428  lmconst  23486  cndis  23516  pnrmopn  23568  cmpfi  23633  finptfin  23744  comppfsc  23758  ptbasfi  23807  pttoponconst  23823  ptcnplem  23847  pthaus  23864  xkoptsub  23880  xkopt  23881  nrmr0reg  23975  ordthmeolem  24027  fbssfi  24063  filconn  24109  hausflim  24207  cnpflf  24227  fclscf  24251  cnpfcf  24267  alexsublem  24270  ptcmplem2  24279  ptcmplem3  24280  tsmsfbas  24354  eltsms  24359  utopbas  24461  isucn2  24504  psmetutop  24793  nrginvrcn  24918  lebnumlem3  25191  fmcfil  25500  ovolicc2lem4  25748  mbfconst  25861  i1fmul  25924  itg2const  25968  itg2cnlem2  25990  itgle  26037  ibladdlem  26047  iblabs  26056  iblabsr  26057  iblmulc2  26058  bddmulibl  26066  bddiblnc  26069  ellimc2  26104  limcnlp  26105  c1lip1  26224  itgpowd  26277  ply1nzb  26348  ulm0  26627  itgulm2  26645  dchrhash  27507  lgsquadlem2  27617  2sqlem10  27664  dchrisum  27728  rpvmasum2  27748  pntlemj  27839  bday0b  28078  axcontlem12  29432  nbgr0edg  29817  rusgr1vtx  30048  uspgr2wlkeq2  30106  clwwlknondisj  30581  ip2eqi  31337  ubthlem1  31351  hial2eq  31587  pjnmopi  32629  ssmd1  32792  chrelat2i  32846  xrofsup  33238  prodindf  33308  selvply1rhmlemb  34029  extdgfialglem2  34203  ordtrest2NEWlem  34432  truae  34754  mbfmcst  34770  mbfmcnt  34779  dya2iocuni  34794  0rrv  34962  hashreprin  35128  reprgt  35129  breprexplemc  35140  breprexp  35141  circlemeth  35148  hgt750lema  35165  fineqvnttrclselem1  35647  fineqvnttrclse  35650  vonf1wev  35705  vonf1owevOLD  35707  wevgblacfn  35708  onvfowev  35713  cvmliftlem15  35877  satf0suclem  35954  fmla0disjsuc  35977  fmlasucdisj  35978  neibastop2lem  36979  tailf  36994  filnetlem4  37000  fin2so  38361  poimirlem26  38395  poimirlem28  38397  ismblfin  38410  cnambfre  38417  itg2addnclem  38420  itg2addnc  38423  itg2gt0cn  38424  ibladdnclem  38425  iblabsnc  38433  iblmulc2nc  38434  ftc1anclem6  38447  ftc1anclem7  38448  ftc1anclem8  38449  ftc1anc  38450  frinfm  38485  sdclem1  38493  ssbnd  38538  rngoueqz  38690  lssatle  39888  ltrneq2  41021  tendoeq2  41647  lcmineqlem12  42906  hbtlem7  43966  trclrelexplem  44551  rfovcnvf1od  44844  dssmapf1od  44861  neik0pk1imk0  44887  collexd  45081  sswfaxreg  45810  omssaxinf2  45811  prodeq2ad  46422  0cnv  46570  itgperiod  46809  stoweidlem35  46863  stoweidlem59  46887  fourierdlem31  46966  subsaliuncllem  47185  subsaliuncl  47186  iundjiun  47288  hoiprodcl2  47383  ovn0lem  47393  hoidmvlelem3  47425  smflimlem1  47599  smflimlem2  47600  smflimlem3  47601  tmachlem-tpbase  47767  tmachlem-extpcover  47773  tmachlem-agreefin  47776  fundcmpsurinjlem2  48299  sprval  48379  prprval  48414  rmsupp0  49298  lincop  49338  lcoc0  49352  nelsubclem  49993