Theorem ralimi 3073

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3051

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 3052

This theorem is referenced by:  rexbi  3093  ralrexbid  3094  r19.35OLD  3096  r19.26  3098  r19.29OLD  3102  r19.30  3107  2ralimi  3110  3ralimi  3111  4ralimi  3112  5ralimi  3113  6ralimi  3114  r19.21v  3165  rr19.3v  3646  rr19.28v  3647  reu3  3710  uniiunlem  4062  reupick2  4306  ralf0  4489  uniss2  4917  ss2iun  4986  iineq2  4988  dfiun2g  5006  iunss2  5025  disjss2  5089  disjeq2  5090  triin  5246  reusv2lem5  5372  dmmptg  6231  frpoinsg  6332  wfisgOLD  6343  fununi  6610  fnmptf  6673  fnmpt  6677  mpteqb  7004  chfnrn  7038  fvn0ssdmfun  7063  dffo5  7093  ffvresb  7114  fmptcof  7119  mpo2eqb  7537  ralrnmpo  7544  abnexg  7748  tfisg  7847  tfis  7848  fun11uni  7927  fiun  7939  f1iun  7940  zfrep6  7951  mpoexxg  8072  el2mpocsbcl  8082  frxp  8123  xpord2indlem  8144  xpord3inddlem  8151  poseq  8155  smores  8364  naddcllem  8686  naddcom  8692  naddrid  8693  naddunif  8703  naddass  8706  riiner  8802  ixpn0  8942  boxriin  8952  unifi2  9355  wemaplem2  9559  frinsg  9763  rankonidlem  9840  acni3  10059  dfac5  10141  dfac12lem2  10157  kmlem6  10168  kmlem8  10170  kmlem13  10175  cfsmolem  10282  fin23lem40  10363  isf32lem2  10366  fin1a2s  10426  hsmexlem2  10439  hsmex3  10446  axcc4  10451  domtriomlem  10454  dcomex  10459  ac6num  10491  iundom  10554  unirnfdomd  10579  konigthlem  10580  iunctb  10586  gch3  10688  wununi  10718  wunpw  10719  wunpr  10721  eltsk2g  10763  tskpwss  10764  tskpw  10765  grupw  10807  gruurn  10810  intgru  10826  grothpw  10838  grothpwex  10839  grothomex  10841  axgroth3  10843  suplem1pr  11064  supexpr  11066  supsr  11124  fimaxre3  12186  xrsupexmnf  13319  xrinfmexpnf  13320  fsuppmapnn0fiublem  14006  fsuppmapnn0fiub  14007  fsuppmapnn0fiubex  14008  mptnn0fsuppd  14014  rexanre  15363  rexuz3  15365  cau3lem  15371  caubnd2  15374  caubnd  15375  rlim0  15522  rlim0lt  15523  climi2  15525  climi0  15526  climrlim2  15561  rlimres  15572  o1rlimmul  15633  caurcvg  15691  caurcvg2  15692  caucvg  15693  caucvgb  15694  sumeq2  15708  prodeq2  15926  ndvdssub  16426  gcdcllem1  16516  coprmproddvdslem  16679  vdwnnlem1  17013  imasaddfnlem  17540  catidex  17684  catlid  17693  catrid  17694  catcocl  17695  catpropd  17719  subcidcl  17855  funcid  17881  setcepi  18099  tsrss  18597  mgmidmo  18636  gsumval2  18662  isnmnd  18714  issubg2  19122  gagrpid  19275  gaass  19278  cygabl  19870  dprdcntz  19989  dprddisj  19990  abveq0  20776  abvmul  20779  abvtri  20780  psgndiflemB  21558  phllmhm  21590  ipcj  21592  ipeq0  21596  mdetmul  22559  pmatcollpw2lem  22713  eltg2b  22895  iincld  22975  iuncld  22981  isclo2  23024  neips  23049  neipeltop  23065  lmcvg  23198  t1t0  23284  hauscmplem  23342  bwth  23346  1stcelcls  23397  ptuni2  23512  pttopon  23532  ptcld  23549  ptcnplem  23557  txtube  23576  txlm  23584  xkococnlem  23595  fbun  23776  isfil2  23792  ptcmplem4  23991  ustssel  24142  isucn2  24215  ucncn  24221  metrest  24461  tngngp  24591  tngngp3  24593  ncvsi  25101  iscau4  25229  cmetcaulem  25238  caussi  25247  volfiniun  25498  iunmbl  25504  voliun  25505  mbfdm  25577  itg2seq  25693  itg2i1fseqle  25705  itg2i1fseq2  25707  iblcnlem  25740  limcresi  25836  limciun  25845  rolle  25944  ulmss  26356  rlimcnp  26925  madebdayim  27843  addsuniflem  27951  colinearalg  28835  axpasch  28866  axeuclid  28888  axcontlem2  28890  axcontlem4  28892  axcontlem7  28895  axcontlem8  28896  fusgrregdegfi  29495  0grrgr  29506  rusgr1vtxlem  29513  wlkvtxeledg  29550  wlkdlem3  29610  wlkdlem4  29611  lfgriswlk  29614  lfgrwlknloop  29615  eulercrct  30169  1to3vfriendship  30208  frgrregorufr0  30251  isgrpo  30424  grpoidinv  30435  grpoideu  30436  grpoidval  30440  grpoidinv2  30442  vcidOLD  30491  vcdi  30492  vcdir  30493  vcass  30494  nvs  30590  nvz  30596  nvtri  30597  mdbr3  32224  mdbr4  32225  mdsl1i  32248  dmdbr6ati  32350  dmdbr7ati  32351  disjunsn  32521  hasheuni  34062  sigaclcu2  34097  prsiga  34108  measvunilem  34189  cntmeas  34203  omssubadd  34278  signsply0  34529  bnj1498  35038  nummin  35068  lfuhgr2  35087  cvmsdisj  35238  cvmshmeo  35239  cvmliftlem15  35266  cvmlift2lem12  35282  untangtr  35677  elpotr  35745  dfon2lem7  35753  dfon2lem8  35754  opnrebl2  36285  fnemeet2  36331  fnejoin1  36332  fnejoin2  36333  weiunso  36430  weiunse  36432  weiunwe  36433  dfgcd3  37288  domalom  37368  ctbssinf  37370  nlpfvineqsn  37373  fvineqsnf1  37374  pibt1  37380  pibt2  37381  ptrecube  37590  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  heicant  37625  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  frinfm  37705  caushft  37731  sstotbnd3  37746  prdstotbnd  37764  heibor1lem  37779  bfplem2  37793  opidonOLD  37822  exidu1  37826  grpomndo  37845  rngoideu  37873  rngodi  37874  rngodir  37875  rngoass  37876  rngoueqz  37910  idladdcl  37989  idllmulcl  37990  idlrmulcl  37991  mpobi123f  38132  iineq12f  38134  mptbi12f  38136  pmapglbx  39734  ltrnnid  40101  cdlemefrs32fva  40365  unitscyglem3  42156  fsuppind  42560  dffltz  42604  lerabdioph  42775  ltrabdioph  42778  nerabdioph  42779  dvdsrabdioph  42780  rencldnfi  42791  dford3  42999  pwelg  43531  pwinfi2  43533  ss2iundf  43630  neik0imk0p  44007  gneispace  44105  gneispace0nelrn  44111  ismnushort  44273  ralbidar  44417  rexbidar  44418  ssclaxsep  44955  uniclaxun  44959  uzubico2  45545  climuzlem  45720  xlimxrre  45808  natlocalincr  46853  2reuimp0  47091  bgoldbtbndlem2  47768  bgoldbtbndlem4  47770  mpoexxg2  48261  iuneqconst2  48749  iineqconst2  48750  iunord  49488