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 2113  ∀wral 3051

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

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

This theorem is referenced by:  rexbi  3092  ralrexbid  3093  r19.26  3096  r19.30  3103  2ralimi  3106  3ralimi  3107  4ralimi  3108  5ralimi  3109  6ralimi  3110  r19.21v  3161  rr19.3v  3621  rr19.28v  3622  reu3  3685  uniiunlem  4039  reupick2  4283  uniss2  4897  ss2iun  4965  iineq2  4967  dfiun2g  4985  iunss2  5005  disjss2  5068  disjeq2  5069  triin  5221  reusv2lem5  5347  dmmptg  6200  frpoinsg  6301  fununi  6567  fnmptf  6628  fnmpt  6632  mpteqb  6960  chfnrn  6994  fvn0ssdmfun  7019  dffo5  7049  ffvresb  7070  fmptcof  7075  mpo2eqb  7490  ralrnmpo  7497  abnexg  7701  tfisg  7796  tfis  7797  fun11uni  7875  fiun  7887  f1iun  7888  zfrep6  7899  mpoexxg  8019  el2mpocsbcl  8027  frxp  8068  xpord2indlem  8089  xpord3inddlem  8096  poseq  8100  smores  8284  naddcllem  8604  naddcom  8610  naddrid  8611  naddunif  8621  naddass  8624  riiner  8727  ixpn0  8868  boxriin  8878  unifi2  9245  wemaplem2  9452  frinsg  9663  rankonidlem  9740  acni3  9957  dfac5  10039  dfac12lem2  10055  kmlem6  10066  kmlem8  10068  kmlem13  10073  cfsmolem  10180  fin23lem40  10261  isf32lem2  10264  fin1a2s  10324  hsmexlem2  10337  hsmex3  10344  axcc4  10349  domtriomlem  10352  dcomex  10357  ac6num  10389  iundom  10452  unirnfdomd  10478  konigthlem  10479  iunctb  10485  gch3  10587  wununi  10617  wunpw  10618  wunpr  10620  eltsk2g  10662  tskpwss  10663  tskpw  10664  grupw  10706  gruurn  10709  intgru  10725  grothpw  10737  grothpwex  10738  grothomex  10740  axgroth3  10742  suplem1pr  10963  supexpr  10965  supsr  11023  fimaxre3  12088  xrsupexmnf  13220  xrinfmexpnf  13221  fsuppmapnn0fiublem  13913  fsuppmapnn0fiub  13914  fsuppmapnn0fiubex  13915  mptnn0fsuppd  13921  rexanre  15270  rexuz3  15272  cau3lem  15278  caubnd2  15281  caubnd  15282  rlim0  15431  rlim0lt  15432  climi2  15434  climi0  15435  climrlim2  15470  rlimres  15481  o1rlimmul  15542  caurcvg  15600  caurcvg2  15601  caucvg  15602  caucvgb  15603  sumeq2  15617  prodeq2  15835  ndvdssub  16336  gcdcllem1  16426  coprmproddvdslem  16589  vdwnnlem1  16923  imasaddfnlem  17449  catidex  17597  catlid  17606  catrid  17607  catcocl  17608  catpropd  17632  subcidcl  17768  funcid  17794  setcepi  18012  tsrss  18512  mgmidmo  18585  gsumval2  18611  isnmnd  18663  issubg2  19071  gagrpid  19223  gaass  19226  cygabl  19820  dprdcntz  19939  dprddisj  19940  abveq0  20751  abvmul  20754  abvtri  20755  psgndiflemB  21555  phllmhm  21587  ipcj  21589  ipeq0  21593  mdetmul  22567  pmatcollpw2lem  22721  eltg2b  22903  iincld  22983  iuncld  22989  isclo2  23032  neips  23057  neipeltop  23073  lmcvg  23206  t1t0  23292  hauscmplem  23350  bwth  23354  1stcelcls  23405  ptuni2  23520  pttopon  23540  ptcld  23557  ptcnplem  23565  txtube  23584  txlm  23592  xkococnlem  23603  fbun  23784  isfil2  23800  ptcmplem4  23999  ustssel  24150  isucn2  24222  ucncn  24228  metrest  24468  tngngp  24598  tngngp3  24600  ncvsi  25107  iscau4  25235  cmetcaulem  25244  caussi  25253  volfiniun  25504  iunmbl  25510  voliun  25511  mbfdm  25583  itg2seq  25699  itg2i1fseqle  25711  itg2i1fseq2  25713  iblcnlem  25746  limcresi  25842  limciun  25851  rolle  25950  ulmss  26362  rlimcnp  26931  madebdayim  27884  addsuniflem  27997  oldfib  28373  colinearalg  28983  axpasch  29014  axeuclid  29036  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  axcontlem8  29044  fusgrregdegfi  29643  0grrgr  29654  rusgr1vtxlem  29661  wlkvtxeledg  29697  wlkdlem3  29756  wlkdlem4  29757  lfgriswlk  29760  lfgrwlknloop  29761  eulercrct  30317  1to3vfriendship  30356  frgrregorufr0  30399  isgrpo  30572  grpoidinv  30583  grpoideu  30584  grpoidval  30588  grpoidinv2  30590  vcidOLD  30639  vcdi  30640  vcdir  30641  vcass  30642  nvs  30738  nvz  30744  nvtri  30745  mdbr3  32372  mdbr4  32373  mdsl1i  32396  dmdbr6ati  32498  dmdbr7ati  32499  disjunsn  32669  hasheuni  34242  sigaclcu2  34277  prsiga  34288  measvunilem  34369  cntmeas  34383  omssubadd  34457  signsply0  34708  bnj1498  35217  nummin  35249  tz9.1regs  35290  onvf1odlem4  35300  lfuhgr2  35313  cvmsdisj  35464  cvmshmeo  35465  cvmliftlem15  35492  cvmlift2lem12  35508  untangtr  35908  elpotr  35973  dfon2lem7  35981  dfon2lem8  35982  opnrebl2  36515  fnemeet2  36561  fnejoin1  36562  fnejoin2  36563  weiunso  36660  weiunse  36662  weiunwe  36663  dfgcd3  37529  domalom  37609  ctbssinf  37611  nlpfvineqsn  37614  fvineqsnf1  37615  pibt1  37621  pibt2  37622  ptrecube  37821  poimirlem25  37846  poimirlem26  37847  poimirlem27  37848  poimirlem30  37851  poimirlem31  37852  poimirlem32  37853  heicant  37856  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  frinfm  37936  caushft  37962  sstotbnd3  37977  prdstotbnd  37995  heibor1lem  38010  bfplem2  38024  opidonOLD  38053  exidu1  38057  grpomndo  38076  rngoideu  38104  rngodi  38105  rngodir  38106  rngoass  38107  rngoueqz  38141  idladdcl  38220  idllmulcl  38221  idlrmulcl  38222  mpobi123f  38363  iineq12f  38365  mptbi12f  38367  dmqsblocks  39112  pmapglbx  40029  ltrnnid  40396  cdlemefrs32fva  40660  unitscyglem3  42451  fsuppind  42833  dffltz  42877  lerabdioph  43047  ltrabdioph  43050  nerabdioph  43051  dvdsrabdioph  43052  rencldnfi  43063  dford3  43270  pwelg  43801  pwinfi2  43803  ss2iundf  43900  neik0imk0p  44277  gneispace  44375  gneispace0nelrn  44381  ismnushort  44542  ralbidar  44685  rexbidar  44686  ssclaxsep  45223  uniclaxun  45227  uzubico2  45814  climuzlem  45987  xlimxrre  46075  natlocalincr  47120  2reuimp0  47360  bgoldbtbndlem2  48052  bgoldbtbndlem4  48054  mpoexxg2  48584  iuneqconst2  49068  iineqconst2  49069  iunord  49921