Theorem ralimi 3104

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3082

This theorem is used by:  rexbi  3123  ralrexbid  3124  r19.26  3127  r19.30  3134  2ralimi  3137  3ralimi  3138  4ralimi  3139  5ralimi  3140  6ralimi  3141  r19.21v  3192  rr19.3v  3628  rr19.28v  3629  reu3  3692  uniiunlem  4042  reupick2  4284  uniss2  4909  ss2iun  4977  iineq2  4979  dfiun2g  4996  iunss2  5016  disjss2  5081  disjeq2  5082  triin  5237  replem  5251  zfrep6  5252  reusv2lem5  5375  dmmptg  6245  frpoinsg  6348  fununi  6615  fnmptf  6675  fnmpt  6679  mpteqb  7013  chfnrn  7048  fvn0ssdmfun  7073  dffo5  7103  ffvresb  7125  fmptcof  7130  mpo2eqb  7548  ralrnmpo  7555  abnexg  7757  tfisg  7852  tfis  7853  fun11uni  7932  fiun  7942  f1iun  7943  zfrep6OLD  7954  mpoexxg  8074  el2mpocsbcl  8082  frxp  8124  xpord2indlem  8145  xpord3inddlem  8152  poseq  8156  smores  8341  naddcllem  8664  naddcom  8671  naddrid  8672  naddunif  8682  naddass  8685  riiner  8790  ixpn0  8930  boxriin  8940  unifi2  9305  wemaplem2  9512  frinsg  9726  rankonidlem  9803  acni3  10043  dfac5  10124  dfac12lem2  10140  kmlem6  10151  kmlem8  10153  kmlem13  10158  cfsmolem  10265  fin23lem40  10346  isf32lem2  10349  fin1a2s  10409  hsmexlem2  10422  hsmex3  10429  axcc4  10434  domtriomlem  10437  dcomex  10442  ac6num  10474  iundom  10537  unirnfdomd  10563  konigthlem  10564  iunctb  10570  gch3  10672  wununi  10702  wunpw  10703  wunpr  10705  eltsk2g  10747  tskpwss  10748  tskpw  10749  grupw  10791  gruurn  10794  intgru  10810  grothpw  10822  grothpwex  10823  grothomex  10825  axgroth3  10827  suplem1pr  11048  supexpr  11050  supsr  11108  fimaxre3  12172  xrsupexmnf  13342  xrinfmexpnf  13343  fsuppmapnn0fiublem  14039  fsuppmapnn0fiub  14040  fsuppmapnn0fiubex  14041  mptnn0fsuppd  14047  rexanre  15417  rexuz3  15419  cau3lem  15425  caubnd2  15428  caubnd  15429  rlim0  15578  rlim0lt  15579  climi2  15581  climi0  15582  climrlim2  15617  rlimres  15628  o1rlimmul  15689  caurcvg  15747  caurcvg2  15748  caucvg  15749  caucvgb  15750  sumeq2  15764  prodeq2  15984  ndvdssub  16484  gcdcllem1  16574  coprmproddvdslem  16737  vdwnnlem1  17072  imasaddfnlem  17599  catidex  17747  catlid  17756  catrid  17757  catcocl  17758  catpropd  17782  subcidcl  17918  funcid  17944  setcepi  18162  tsrss  18662  mgmidmo  18735  gsumval2  18765  isnmnd  18817  issubg2  19231  gagrpid  19387  gaass  19390  cygabl  19984  dprdcntz  20103  dprddisj  20104  abveq0  20950  abvmul  20953  abvtri  20954  psgndiflemB  21779  phllmhm  21811  ipcj  21813  ipeq0  21817  mdetmul  22809  pmatcollpw2lem  22963  eltg2b  23145  iincld  23225  iuncld  23231  isclo2  23274  neips  23299  neipeltop  23315  lmcvg  23448  t1t0  23534  hauscmplem  23592  bwth  23596  1stcelcls  23647  ptuni2  23762  pttopon  23782  ptcld  23799  ptcnplem  23807  txtube  23826  txlm  23834  xkococnlem  23845  fbun  24026  isfil2  24042  ptcmplem4  24241  ustssel  24392  isucn2  24464  ucncn  24470  metrest  24710  tngngp  24840  tngngp3  24842  ncvsi  25339  iscau4  25467  cmetcaulem  25476  caussi  25485  volfiniun  25735  iunmbl  25741  voliun  25742  mbfdm  25814  itg2seq  25930  itg2i1fseqle  25942  itg2i1fseq2  25944  iblcnlem  25977  limcresi  26073  limciun  26082  rolle  26178  ulmss  26589  rlimcnp  27159  madebdayim  28110  addsuniflem  28223  oldfib  28599  colinearalg  29289  axpasch  29320  axeuclid  29342  axcontlem2  29344  axcontlem4  29346  axcontlem7  29349  axcontlem8  29350  fusgrregdegfi  29948  0grrgr  29959  rusgr1vtxlem  29966  wlkvtxeledg  30002  wlkdlem3  30061  wlkdlem4  30062  lfgriswlk  30065  lfgrwlknloop  30066  eulercrct  30622  1to3vfriendship  30661  frgrregorufr0  30704  isgrpo  30878  grpoidinv  30889  grpoideu  30890  grpoidval  30894  grpoidinv2  30896  vcidOLD  30945  vcdi  30946  vcdir  30947  vcass  30948  nvs  31044  nvz  31050  nvtri  31051  mdbr3  32678  mdbr4  32679  mdsl1i  32702  dmdbr6ati  32804  dmdbr7ati  32805  disjunsn  32968  hasheuni  34498  sigaclcu2  34533  prsiga  34544  measvunilem  34626  cntmeas  34640  omssubadd  34714  signsply0  34962  bnj1498  35473  nummin  35501  axprALT2  35520  tz9.1regs  35563  onvf1odlem4  35606  lfuhgr2  35624  cvmsdisj  35775  cvmshmeo  35776  cvmliftlem15  35803  cvmlift2lem12  35819  untangtr  36219  elpotr  36284  dfon2lem7  36292  dfon2lem8  36293  nmulprop  36695  opnrebl2  36865  fnemeet2  36911  fnejoin1  36912  fnejoin2  36913  weiunso  37010  weiunse  37012  weiunwe  37013  dfgcd3  38001  domalom  38083  ctbssinf  38085  nlpfvineqsn  38088  fvineqsnf1  38089  pibt1  38095  pibt2  38096  ptrecube  38304  poimirlem25  38329  poimirlem26  38330  poimirlem27  38331  poimirlem30  38334  poimirlem31  38335  poimirlem32  38336  heicant  38339  ovoliunnfl  38346  voliunnfl  38348  volsupnfl  38349  frinfm  38419  caushft  38445  sstotbnd3  38460  prdstotbnd  38478  heibor1lem  38493  bfplem2  38507  opidonOLD  38536  exidu1  38540  grpomndo  38559  rngoideu  38587  rngodi  38588  rngodir  38589  rngoass  38590  rngoueqz  38624  idladdcl  38703  idllmulcl  38704  idlrmulcl  38705  mpobi123f  38844  iineq12f  38846  mptbi12f  38848  dmqsblocks  39649  pmapglbx  40576  ltrnnid  40943  cdlemefrs32fva  41207  unitscyglem3  42997  fsuppind  43355  dffltz  43399  lerabdioph  43565  ltrabdioph  43568  nerabdioph  43569  dvdsrabdioph  43570  rencldnfi  43581  dford3  43788  pwelg  44319  pwinfi2  44321  ss2iundf  44418  neik0imk0p  44795  gneispace  44893  gneispace0nelrn  44899  ismnushort  45044  ralbidar  45187  rexbidar  45188  ssclaxsep  45724  uniclaxun  45728  uzubico2  46317  climuzlem  46490  xlimxrre  46578  natlocalincr  47625  2reuimp0  47884  bgoldbtbndlem2  48604  bgoldbtbndlem4  48606  mpoexxg2  49151  iuneqconst2  49634  iineqconst2  49635  iunord  50487