Theorem ralimi 3083

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

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

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 3062

This theorem is referenced by:  rexbi  3104  ralrexbid  3106  r19.35OLD  3109  r19.26  3111  r19.29OLD  3115  r19.30  3120  r19.30OLD  3121  2ralimi  3123  3ralimi  3124  4ralimi  3125  5ralimi  3126  6ralimi  3127  r19.21v  3180  rr19.3v  3667  rr19.28v  3668  reu3  3733  uniiunlem  4087  reupick2  4331  ralf0  4514  uniss2  4941  ss2iun  5010  iineq2  5012  dfiun2g  5030  iunss2  5049  disjss2  5113  disjeq2  5114  triin  5276  reusv2lem5  5402  dmmptg  6262  frpoinsg  6364  wfisgOLD  6375  fununi  6641  fnmptf  6704  fnmpt  6708  mpteqb  7035  chfnrn  7069  fvn0ssdmfun  7094  dffo5  7124  ffvresb  7145  fmptcof  7150  mpo2eqb  7565  ralrnmpo  7572  abnexg  7776  tfisg  7875  tfis  7876  fun11uni  7955  fiun  7967  f1iun  7968  zfrep6  7979  mpoexxg  8100  el2mpocsbcl  8110  frxp  8151  xpord2indlem  8172  xpord3inddlem  8179  poseq  8183  smores  8392  naddcllem  8714  naddcom  8720  naddrid  8721  naddunif  8731  naddass  8734  riiner  8830  ixpn0  8970  boxriin  8980  unifi2  9385  wemaplem2  9587  frinsg  9791  rankonidlem  9868  acni3  10087  dfac5  10169  dfac12lem2  10185  kmlem6  10196  kmlem8  10198  kmlem13  10203  cfsmolem  10310  fin23lem40  10391  isf32lem2  10394  fin1a2s  10454  hsmexlem2  10467  hsmex3  10474  axcc4  10479  domtriomlem  10482  dcomex  10487  ac6num  10519  iundom  10582  unirnfdomd  10607  konigthlem  10608  iunctb  10614  gch3  10716  wununi  10746  wunpw  10747  wunpr  10749  eltsk2g  10791  tskpwss  10792  tskpw  10793  grupw  10835  gruurn  10838  intgru  10854  grothpw  10866  grothpwex  10867  grothomex  10869  axgroth3  10871  suplem1pr  11092  supexpr  11094  supsr  11152  fimaxre3  12214  xrsupexmnf  13347  xrinfmexpnf  13348  fsuppmapnn0fiublem  14031  fsuppmapnn0fiub  14032  fsuppmapnn0fiubex  14033  mptnn0fsuppd  14039  rexanre  15385  rexuz3  15387  cau3lem  15393  caubnd2  15396  caubnd  15397  rlim0  15544  rlim0lt  15545  climi2  15547  climi0  15548  climrlim2  15583  rlimres  15594  o1rlimmul  15655  caurcvg  15713  caurcvg2  15714  caucvg  15715  caucvgb  15716  sumeq2  15730  prodeq2  15948  ndvdssub  16446  gcdcllem1  16536  coprmproddvdslem  16699  vdwnnlem1  17033  imasaddfnlem  17573  catidex  17717  catlid  17726  catrid  17727  catcocl  17728  catpropd  17752  subcidcl  17889  funcid  17915  setcepi  18133  tsrss  18634  mgmidmo  18673  gsumval2  18699  isnmnd  18751  issubg2  19159  gagrpid  19312  gaass  19315  cygabl  19909  dprdcntz  20028  dprddisj  20029  abveq0  20819  abvmul  20822  abvtri  20823  psgndiflemB  21618  phllmhm  21650  ipcj  21652  ipeq0  21656  mdetmul  22629  pmatcollpw2lem  22783  eltg2b  22966  iincld  23047  iuncld  23053  isclo2  23096  neips  23121  neipeltop  23137  lmcvg  23270  t1t0  23356  hauscmplem  23414  bwth  23418  1stcelcls  23469  ptuni2  23584  pttopon  23604  ptcld  23621  ptcnplem  23629  txtube  23648  txlm  23656  xkococnlem  23667  fbun  23848  isfil2  23864  ptcmplem4  24063  ustssel  24214  isucn2  24288  ucncn  24294  metrest  24537  tngngp  24675  tngngp3  24677  ncvsi  25185  iscau4  25313  cmetcaulem  25322  caussi  25331  volfiniun  25582  iunmbl  25588  voliun  25589  mbfdm  25661  itg2seq  25777  itg2i1fseqle  25789  itg2i1fseq2  25791  iblcnlem  25824  limcresi  25920  limciun  25929  rolle  26028  ulmss  26440  rlimcnp  27008  madebdayim  27926  addsuniflem  28034  colinearalg  28925  axpasch  28956  axeuclid  28978  axcontlem2  28980  axcontlem4  28982  axcontlem7  28985  axcontlem8  28986  fusgrregdegfi  29587  0grrgr  29598  rusgr1vtxlem  29605  wlkvtxeledg  29642  wlkdlem3  29702  wlkdlem4  29703  lfgriswlk  29706  lfgrwlknloop  29707  eulercrct  30261  1to3vfriendship  30300  frgrregorufr0  30343  isgrpo  30516  grpoidinv  30527  grpoideu  30528  grpoidval  30532  grpoidinv2  30534  vcidOLD  30583  vcdi  30584  vcdir  30585  vcass  30586  nvs  30682  nvz  30688  nvtri  30689  mdbr3  32316  mdbr4  32317  mdsl1i  32340  dmdbr6ati  32442  dmdbr7ati  32443  disjunsn  32607  hasheuni  34086  sigaclcu2  34121  prsiga  34132  measvunilem  34213  cntmeas  34227  omssubadd  34302  signsply0  34566  bnj1498  35075  nummin  35105  lfuhgr2  35124  cvmsdisj  35275  cvmshmeo  35276  cvmliftlem15  35303  cvmlift2lem12  35319  untangtr  35714  elpotr  35782  dfon2lem7  35790  dfon2lem8  35791  opnrebl2  36322  fnemeet2  36368  fnejoin1  36369  fnejoin2  36370  weiunso  36467  weiunse  36469  weiunwe  36470  dfgcd3  37325  domalom  37405  ctbssinf  37407  nlpfvineqsn  37410  fvineqsnf1  37411  pibt1  37417  pibt2  37418  ptrecube  37627  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  heicant  37662  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  frinfm  37742  caushft  37768  sstotbnd3  37783  prdstotbnd  37801  heibor1lem  37816  bfplem2  37830  opidonOLD  37859  exidu1  37863  grpomndo  37882  rngoideu  37910  rngodi  37911  rngodir  37912  rngoass  37913  rngoueqz  37947  idladdcl  38026  idllmulcl  38027  idlrmulcl  38028  mpobi123f  38169  iineq12f  38171  mptbi12f  38173  pmapglbx  39771  ltrnnid  40138  cdlemefrs32fva  40402  unitscyglem3  42198  fsuppind  42600  dffltz  42644  lerabdioph  42816  ltrabdioph  42819  nerabdioph  42820  dvdsrabdioph  42821  rencldnfi  42832  dford3  43040  pwelg  43573  pwinfi2  43575  ss2iundf  43672  neik0imk0p  44049  gneispace  44147  gneispace0nelrn  44153  ismnushort  44320  ralbidar  44464  rexbidar  44465  ssclaxsep  44999  uniclaxun  45003  uzubico2  45583  climuzlem  45758  xlimxrre  45846  natlocalincr  46891  2reuimp0  47126  bgoldbtbndlem2  47793  bgoldbtbndlem4  47795  mpoexxg2  48254  iunord  49195