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 2106  ∀wral 3061

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

This theorem depends on definitions:  df-bi 206  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  3179  rr19.3v  3656  rr19.28v  3657  reu3  3722  uniiunlem  4083  reupick2  4319  ralf0  4512  uniss2  4944  ss2iun  5014  iineq2  5016  dfiun2g  5032  iunss2  5051  disjss2  5115  disjeq2  5116  triin  5281  reusv2lem5  5399  dmmptg  6238  frpoinsg  6341  wfisgOLD  6352  fununi  6620  fnmptf  6683  fnmpt  6687  mpteqb  7014  chfnrn  7047  fvn0ssdmfun  7073  dffo5  7102  ffvresb  7120  fmptcof  7124  mpo2eqb  7537  ralrnmpo  7543  abnexg  7739  tfisg  7839  tfis  7840  fun11uni  7919  fiun  7925  f1iun  7926  zfrep6  7937  mpoexxg  8058  el2mpocsbcl  8067  frxp  8108  xpord2indlem  8129  xpord3inddlem  8136  poseq  8140  smores  8348  naddcllem  8671  naddcom  8677  naddrid  8678  naddunif  8688  naddass  8691  riiner  8780  ixpn0  8920  boxriin  8930  unifi2  9338  wemaplem2  9538  frinsg  9742  rankonidlem  9819  acni3  10038  dfac5  10119  dfac12lem2  10135  kmlem6  10146  kmlem8  10148  kmlem13  10153  cfsmolem  10261  fin23lem40  10342  isf32lem2  10345  fin1a2s  10405  hsmexlem2  10418  hsmex3  10425  axcc4  10430  domtriomlem  10433  dcomex  10438  ac6num  10470  iundom  10533  unirnfdomd  10558  konigthlem  10559  iunctb  10565  gch3  10667  wununi  10697  wunpw  10698  wunpr  10700  eltsk2g  10742  tskpwss  10743  tskpw  10744  grupw  10786  gruurn  10789  intgru  10805  grothpw  10817  grothpwex  10818  grothomex  10820  axgroth3  10822  suplem1pr  11043  supexpr  11045  supsr  11103  fimaxre3  12156  xrsupexmnf  13280  xrinfmexpnf  13281  fsuppmapnn0fiublem  13951  fsuppmapnn0fiub  13952  fsuppmapnn0fiubex  13953  mptnn0fsuppd  13959  rexanre  15289  rexuz3  15291  cau3lem  15297  caubnd2  15300  caubnd  15301  rlim0  15448  rlim0lt  15449  climi2  15451  climi0  15452  climrlim2  15487  rlimres  15498  o1rlimmul  15559  caurcvg  15619  caurcvg2  15620  caucvg  15621  caucvgb  15622  sumeq2  15636  prodeq2  15854  ndvdssub  16348  gcdcllem1  16436  coprmproddvdslem  16595  vdwnnlem1  16924  imasaddfnlem  17470  catidex  17614  catlid  17623  catrid  17624  catcocl  17625  catpropd  17649  subcidcl  17790  funcid  17816  setcepi  18034  tsrss  18538  mgmidmo  18575  gsumval2  18601  isnmnd  18625  issubg2  19015  gagrpid  19152  gaass  19155  cygabl  19753  dprdcntz  19872  dprddisj  19873  abveq0  20426  abvmul  20429  abvtri  20430  psgndiflemB  21144  phllmhm  21176  ipcj  21178  ipeq0  21182  mdetmul  22116  pmatcollpw2lem  22270  eltg2b  22453  iincld  22534  iuncld  22540  isclo2  22583  neips  22608  neipeltop  22624  lmcvg  22757  t1t0  22843  hauscmplem  22901  bwth  22905  1stcelcls  22956  ptuni2  23071  pttopon  23091  ptcld  23108  ptcnplem  23116  txtube  23135  txlm  23143  xkococnlem  23154  fbun  23335  isfil2  23351  ptcmplem4  23550  ustssel  23701  isucn2  23775  ucncn  23781  metrest  24024  tngngp  24162  tngngp3  24164  ncvsi  24659  iscau4  24787  cmetcaulem  24796  caussi  24805  volfiniun  25055  iunmbl  25061  voliun  25062  mbfdm  25134  itg2seq  25251  itg2i1fseqle  25263  itg2i1fseq2  25265  iblcnlem  25297  limcresi  25393  limciun  25402  rolle  25498  ulmss  25900  rlimcnp  26459  madebdayim  27371  addsuniflem  27473  colinearalg  28157  axpasch  28188  axeuclid  28210  axcontlem2  28212  axcontlem4  28214  axcontlem7  28217  axcontlem8  28218  fusgrregdegfi  28815  0grrgr  28826  rusgr1vtxlem  28833  wlkvtxeledg  28870  wlkdlem3  28930  wlkdlem4  28931  lfgriswlk  28934  lfgrwlknloop  28935  eulercrct  29484  1to3vfriendship  29523  frgrregorufr0  29566  isgrpo  29737  grpoidinv  29748  grpoideu  29749  grpoidval  29753  grpoidinv2  29755  vcidOLD  29804  vcdi  29805  vcdir  29806  vcass  29807  nvs  29903  nvz  29909  nvtri  29910  mdbr3  31537  mdbr4  31538  mdsl1i  31561  dmdbr6ati  31663  dmdbr7ati  31664  disjunsn  31812  hasheuni  33071  sigaclcu2  33106  prsiga  33117  measvunilem  33198  cntmeas  33212  omssubadd  33287  signsply0  33550  bnj1498  34060  nummin  34082  lfuhgr2  34097  cvmsdisj  34249  cvmshmeo  34250  cvmliftlem15  34277  cvmlift2lem12  34293  untangtr  34671  elpotr  34741  dfon2lem7  34749  dfon2lem8  34750  opnrebl2  35194  fnemeet2  35240  fnejoin1  35241  fnejoin2  35242  dfgcd3  36193  domalom  36273  ctbssinf  36275  nlpfvineqsn  36278  fvineqsnf1  36279  pibt1  36285  pibt2  36286  ptrecube  36476  poimirlem25  36501  poimirlem26  36502  poimirlem27  36503  poimirlem30  36506  poimirlem31  36507  poimirlem32  36508  heicant  36511  ovoliunnfl  36518  voliunnfl  36520  volsupnfl  36521  frinfm  36591  caushft  36617  sstotbnd3  36632  prdstotbnd  36650  heibor1lem  36665  bfplem2  36679  opidonOLD  36708  exidu1  36712  grpomndo  36731  rngoideu  36759  rngodi  36760  rngodir  36761  rngoass  36762  rngoueqz  36796  idladdcl  36875  idllmulcl  36876  idlrmulcl  36877  mpobi123f  37018  iineq12f  37020  mptbi12f  37022  pmapglbx  38628  ltrnnid  38995  cdlemefrs32fva  39259  fsuppind  41159  dffltz  41372  lerabdioph  41528  ltrabdioph  41531  nerabdioph  41532  dvdsrabdioph  41533  rencldnfi  41544  dford3  41752  pwelg  42296  pwinfi2  42298  ss2iundf  42395  neik0imk0p  42772  gneispace  42870  gneispace0nelrn  42876  ismnushort  43045  ralbidar  43189  rexbidar  43190  uzubico2  44269  climuzlem  44445  xlimxrre  44533  natlocalincr  45576  2reuimp0  45808  bgoldbtbndlem2  46460  bgoldbtbndlem4  46462  mpoexxg2  46966  iunord  47674