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  3630  rr19.28v  3631  reu3  3695  uniiunlem  4046  reupick2  4290  ralf0  4473  uniss2  4901  ss2iun  4970  iineq2  4972  dfiun2g  4990  iunss2  5008  disjss2  5072  disjeq2  5073  triin  5226  reusv2lem5  5352  dmmptg  6203  frpoinsg  6304  fununi  6575  fnmptf  6636  fnmpt  6640  mpteqb  6969  chfnrn  7003  fvn0ssdmfun  7028  dffo5  7058  ffvresb  7079  fmptcof  7084  mpo2eqb  7501  ralrnmpo  7508  abnexg  7712  tfisg  7810  tfis  7811  fun11uni  7889  fiun  7901  f1iun  7902  zfrep6  7913  mpoexxg  8033  el2mpocsbcl  8041  frxp  8082  xpord2indlem  8103  xpord3inddlem  8110  poseq  8114  smores  8298  naddcllem  8617  naddcom  8623  naddrid  8624  naddunif  8634  naddass  8637  riiner  8740  ixpn0  8880  boxriin  8890  unifi2  9272  wemaplem2  9476  frinsg  9680  rankonidlem  9757  acni3  9976  dfac5  10058  dfac12lem2  10074  kmlem6  10085  kmlem8  10087  kmlem13  10092  cfsmolem  10199  fin23lem40  10280  isf32lem2  10283  fin1a2s  10343  hsmexlem2  10356  hsmex3  10363  axcc4  10368  domtriomlem  10371  dcomex  10376  ac6num  10408  iundom  10471  unirnfdomd  10496  konigthlem  10497  iunctb  10503  gch3  10605  wununi  10635  wunpw  10636  wunpr  10638  eltsk2g  10680  tskpwss  10681  tskpw  10682  grupw  10724  gruurn  10727  intgru  10743  grothpw  10755  grothpwex  10756  grothomex  10758  axgroth3  10760  suplem1pr  10981  supexpr  10983  supsr  11041  fimaxre3  12105  xrsupexmnf  13241  xrinfmexpnf  13242  fsuppmapnn0fiublem  13931  fsuppmapnn0fiub  13932  fsuppmapnn0fiubex  13933  mptnn0fsuppd  13939  rexanre  15289  rexuz3  15291  cau3lem  15297  caubnd2  15300  caubnd  15301  rlim0  15450  rlim0lt  15451  climi2  15453  climi0  15454  climrlim2  15489  rlimres  15500  o1rlimmul  15561  caurcvg  15619  caurcvg2  15620  caucvg  15621  caucvgb  15622  sumeq2  15636  prodeq2  15854  ndvdssub  16355  gcdcllem1  16445  coprmproddvdslem  16608  vdwnnlem1  16942  imasaddfnlem  17467  catidex  17611  catlid  17620  catrid  17621  catcocl  17622  catpropd  17646  subcidcl  17782  funcid  17808  setcepi  18026  tsrss  18524  mgmidmo  18563  gsumval2  18589  isnmnd  18641  issubg2  19049  gagrpid  19202  gaass  19205  cygabl  19797  dprdcntz  19916  dprddisj  19917  abveq0  20703  abvmul  20706  abvtri  20707  psgndiflemB  21485  phllmhm  21517  ipcj  21519  ipeq0  21523  mdetmul  22486  pmatcollpw2lem  22640  eltg2b  22822  iincld  22902  iuncld  22908  isclo2  22951  neips  22976  neipeltop  22992  lmcvg  23125  t1t0  23211  hauscmplem  23269  bwth  23273  1stcelcls  23324  ptuni2  23439  pttopon  23459  ptcld  23476  ptcnplem  23484  txtube  23503  txlm  23511  xkococnlem  23522  fbun  23703  isfil2  23719  ptcmplem4  23918  ustssel  24069  isucn2  24142  ucncn  24148  metrest  24388  tngngp  24518  tngngp3  24520  ncvsi  25027  iscau4  25155  cmetcaulem  25164  caussi  25173  volfiniun  25424  iunmbl  25430  voliun  25431  mbfdm  25503  itg2seq  25619  itg2i1fseqle  25631  itg2i1fseq2  25633  iblcnlem  25666  limcresi  25762  limciun  25771  rolle  25870  ulmss  26282  rlimcnp  26851  madebdayim  27775  addsuniflem  27884  colinearalg  28813  axpasch  28844  axeuclid  28866  axcontlem2  28868  axcontlem4  28870  axcontlem7  28873  axcontlem8  28874  fusgrregdegfi  29473  0grrgr  29484  rusgr1vtxlem  29491  wlkvtxeledg  29527  wlkdlem3  29586  wlkdlem4  29587  lfgriswlk  29590  lfgrwlknloop  29591  eulercrct  30144  1to3vfriendship  30183  frgrregorufr0  30226  isgrpo  30399  grpoidinv  30410  grpoideu  30411  grpoidval  30415  grpoidinv2  30417  vcidOLD  30466  vcdi  30467  vcdir  30468  vcass  30469  nvs  30565  nvz  30571  nvtri  30572  mdbr3  32199  mdbr4  32200  mdsl1i  32223  dmdbr6ati  32325  dmdbr7ati  32326  disjunsn  32496  hasheuni  34048  sigaclcu2  34083  prsiga  34094  measvunilem  34175  cntmeas  34189  omssubadd  34264  signsply0  34515  bnj1498  35024  nummin  35054  onvf1odlem4  35066  lfuhgr2  35079  cvmsdisj  35230  cvmshmeo  35231  cvmliftlem15  35258  cvmlift2lem12  35274  untangtr  35674  elpotr  35742  dfon2lem7  35750  dfon2lem8  35751  opnrebl2  36282  fnemeet2  36328  fnejoin1  36329  fnejoin2  36330  weiunso  36427  weiunse  36429  weiunwe  36430  dfgcd3  37285  domalom  37365  ctbssinf  37367  nlpfvineqsn  37370  fvineqsnf1  37371  pibt1  37377  pibt2  37378  ptrecube  37587  poimirlem25  37612  poimirlem26  37613  poimirlem27  37614  poimirlem30  37617  poimirlem31  37618  poimirlem32  37619  heicant  37622  ovoliunnfl  37629  voliunnfl  37631  volsupnfl  37632  frinfm  37702  caushft  37728  sstotbnd3  37743  prdstotbnd  37761  heibor1lem  37776  bfplem2  37790  opidonOLD  37819  exidu1  37823  grpomndo  37842  rngoideu  37870  rngodi  37871  rngodir  37872  rngoass  37873  rngoueqz  37907  idladdcl  37986  idllmulcl  37987  idlrmulcl  37988  mpobi123f  38129  iineq12f  38131  mptbi12f  38133  dmqsblocks  38818  pmapglbx  39736  ltrnnid  40103  cdlemefrs32fva  40367  unitscyglem3  42158  fsuppind  42551  dffltz  42595  lerabdioph  42766  ltrabdioph  42769  nerabdioph  42770  dvdsrabdioph  42771  rencldnfi  42782  dford3  42990  pwelg  43522  pwinfi2  43524  ss2iundf  43621  neik0imk0p  43998  gneispace  44096  gneispace0nelrn  44102  ismnushort  44263  ralbidar  44407  rexbidar  44408  ssclaxsep  44945  uniclaxun  44949  uzubico2  45539  climuzlem  45714  xlimxrre  45802  natlocalincr  46847  2reuimp0  47088  bgoldbtbndlem2  47780  bgoldbtbndlem4  47782  mpoexxg2  48299  iuneqconst2  48784  iineqconst2  48785  iunord  49638