Theorem ralimi 3066

Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)

Hypothesis

Ref	Expression
ralimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ralimi	⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralimi

Step	Hyp	Ref	Expression
1		ralimi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	ralimia 3063	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

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

This theorem is referenced by:  rexbi  3086  ralrexbid  3087  r19.35OLD  3089  r19.26  3091  r19.29OLD  3095  r19.30  3100  2ralimi  3103  3ralimi  3104  4ralimi  3105  5ralimi  3106  6ralimi  3107  r19.21v  3158  rr19.3v  3633  rr19.28v  3634  reu3  3698  uniiunlem  4050  reupick2  4294  ralf0  4477  uniss2  4905  ss2iun  4974  iineq2  4976  dfiun2g  4994  iunss2  5013  disjss2  5077  disjeq2  5078  triin  5231  reusv2lem5  5357  dmmptg  6215  frpoinsg  6316  fununi  6591  fnmptf  6654  fnmpt  6658  mpteqb  6987  chfnrn  7021  fvn0ssdmfun  7046  dffo5  7076  ffvresb  7097  fmptcof  7102  mpo2eqb  7521  ralrnmpo  7528  abnexg  7732  tfisg  7830  tfis  7831  fun11uni  7909  fiun  7921  f1iun  7922  zfrep6  7933  mpoexxg  8054  el2mpocsbcl  8064  frxp  8105  xpord2indlem  8126  xpord3inddlem  8133  poseq  8137  smores  8321  naddcllem  8640  naddcom  8646  naddrid  8647  naddunif  8657  naddass  8660  riiner  8763  ixpn0  8903  boxriin  8913  unifi2  9296  wemaplem2  9500  frinsg  9704  rankonidlem  9781  acni3  10000  dfac5  10082  dfac12lem2  10098  kmlem6  10109  kmlem8  10111  kmlem13  10116  cfsmolem  10223  fin23lem40  10304  isf32lem2  10307  fin1a2s  10367  hsmexlem2  10380  hsmex3  10387  axcc4  10392  domtriomlem  10395  dcomex  10400  ac6num  10432  iundom  10495  unirnfdomd  10520  konigthlem  10521  iunctb  10527  gch3  10629  wununi  10659  wunpw  10660  wunpr  10662  eltsk2g  10704  tskpwss  10705  tskpw  10706  grupw  10748  gruurn  10751  intgru  10767  grothpw  10779  grothpwex  10780  grothomex  10782  axgroth3  10784  suplem1pr  11005  supexpr  11007  supsr  11065  fimaxre3  12129  xrsupexmnf  13265  xrinfmexpnf  13266  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  fsuppmapnn0fiubex  13957  mptnn0fsuppd  13963  rexanre  15313  rexuz3  15315  cau3lem  15321  caubnd2  15324  caubnd  15325  rlim0  15474  rlim0lt  15475  climi2  15477  climi0  15478  climrlim2  15513  rlimres  15524  o1rlimmul  15585  caurcvg  15643  caurcvg2  15644  caucvg  15645  caucvgb  15646  sumeq2  15660  prodeq2  15878  ndvdssub  16379  gcdcllem1  16469  coprmproddvdslem  16632  vdwnnlem1  16966  imasaddfnlem  17491  catidex  17635  catlid  17644  catrid  17645  catcocl  17646  catpropd  17670  subcidcl  17806  funcid  17832  setcepi  18050  tsrss  18548  mgmidmo  18587  gsumval2  18613  isnmnd  18665  issubg2  19073  gagrpid  19226  gaass  19229  cygabl  19821  dprdcntz  19940  dprddisj  19941  abveq0  20727  abvmul  20730  abvtri  20731  psgndiflemB  21509  phllmhm  21541  ipcj  21543  ipeq0  21547  mdetmul  22510  pmatcollpw2lem  22664  eltg2b  22846  iincld  22926  iuncld  22932  isclo2  22975  neips  23000  neipeltop  23016  lmcvg  23149  t1t0  23235  hauscmplem  23293  bwth  23297  1stcelcls  23348  ptuni2  23463  pttopon  23483  ptcld  23500  ptcnplem  23508  txtube  23527  txlm  23535  xkococnlem  23546  fbun  23727  isfil2  23743  ptcmplem4  23942  ustssel  24093  isucn2  24166  ucncn  24172  metrest  24412  tngngp  24542  tngngp3  24544  ncvsi  25051  iscau4  25179  cmetcaulem  25188  caussi  25197  volfiniun  25448  iunmbl  25454  voliun  25455  mbfdm  25527  itg2seq  25643  itg2i1fseqle  25655  itg2i1fseq2  25657  iblcnlem  25690  limcresi  25786  limciun  25795  rolle  25894  ulmss  26306  rlimcnp  26875  madebdayim  27799  addsuniflem  27908  colinearalg  28837  axpasch  28868  axeuclid  28890  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  axcontlem8  28898  fusgrregdegfi  29497  0grrgr  29508  rusgr1vtxlem  29515  wlkvtxeledg  29552  wlkdlem3  29612  wlkdlem4  29613  lfgriswlk  29616  lfgrwlknloop  29617  eulercrct  30171  1to3vfriendship  30210  frgrregorufr0  30253  isgrpo  30426  grpoidinv  30437  grpoideu  30438  grpoidval  30442  grpoidinv2  30444  vcidOLD  30493  vcdi  30494  vcdir  30495  vcass  30496  nvs  30592  nvz  30598  nvtri  30599  mdbr3  32226  mdbr4  32227  mdsl1i  32250  dmdbr6ati  32352  dmdbr7ati  32353  disjunsn  32523  hasheuni  34075  sigaclcu2  34110  prsiga  34121  measvunilem  34202  cntmeas  34216  omssubadd  34291  signsply0  34542  bnj1498  35051  nummin  35081  onvf1odlem4  35093  lfuhgr2  35106  cvmsdisj  35257  cvmshmeo  35258  cvmliftlem15  35285  cvmlift2lem12  35301  untangtr  35701  elpotr  35769  dfon2lem7  35777  dfon2lem8  35778  opnrebl2  36309  fnemeet2  36355  fnejoin1  36356  fnejoin2  36357  weiunso  36454  weiunse  36456  weiunwe  36457  dfgcd3  37312  domalom  37392  ctbssinf  37394  nlpfvineqsn  37397  fvineqsnf1  37398  pibt1  37404  pibt2  37405  ptrecube  37614  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  heicant  37649  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  frinfm  37729  caushft  37755  sstotbnd3  37770  prdstotbnd  37788  heibor1lem  37803  bfplem2  37817  opidonOLD  37846  exidu1  37850  grpomndo  37869  rngoideu  37897  rngodi  37898  rngodir  37899  rngoass  37900  rngoueqz  37934  idladdcl  38013  idllmulcl  38014  idlrmulcl  38015  mpobi123f  38156  iineq12f  38158  mptbi12f  38160  dmqsblocks  38845  pmapglbx  39763  ltrnnid  40130  cdlemefrs32fva  40394  unitscyglem3  42185  fsuppind  42578  dffltz  42622  lerabdioph  42793  ltrabdioph  42796  nerabdioph  42797  dvdsrabdioph  42798  rencldnfi  42809  dford3  43017  pwelg  43549  pwinfi2  43551  ss2iundf  43648  neik0imk0p  44025  gneispace  44123  gneispace0nelrn  44129  ismnushort  44290  ralbidar  44434  rexbidar  44435  ssclaxsep  44972  uniclaxun  44976  uzubico2  45566  climuzlem  45741  xlimxrre  45829  natlocalincr  46874  2reuimp0  47115  bgoldbtbndlem2  47807  bgoldbtbndlem4  47809  mpoexxg2  48326  iuneqconst2  48811  iineqconst2  48812  iunord  49665