MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ineq2i Structured version   Visualization version   GIF version

Theorem ineq2i 3803
Description: Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
Hypothesis
Ref Expression
ineq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
ineq2i (𝐶𝐴) = (𝐶𝐵)

Proof of Theorem ineq2i
StepHypRef Expression
1 ineq1i.1 . 2 𝐴 = 𝐵
2 ineq2 3800 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  cin 3566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574
This theorem is referenced by:  in4  3821  inindir  3823  indif2  3862  difun1  3879  dfrab3ss  3897  undif1  4034  difdifdir  4047  dfif3  4091  dfif5  4093  disjpr2  4239  disjprsn  4241  disjtp2  4243  intunsn  4507  rint0  4508  riin0  4585  csbres  5388  res0  5389  resres  5397  resundi  5398  resindi  5400  inres  5402  resiun2  5406  resopab  5434  dffr3  5486  dfse2  5487  dminxp  5562  imainrect  5563  resdmres  5613  dfpred2  5677  predidm  5690  funimacnv  5958  fresaun  6062  fresaunres2  6063  wfrlem13  7412  tfrlem10  7468  sbthlem5  8059  infssuni  8242  dfsup2  8335  en3lplem2  8497  wemapwe  8579  epfrs  8592  r0weon  8820  infxpenlem  8821  kmlem11  8967  ackbij1lem1  9027  ackbij1lem2  9028  axdc3lem4  9260  canthwelem  9457  dmaddpi  9697  dmmulpi  9698  ssxr  10092  dmhashres  13112  fz1isolem  13228  f1oun2prg  13643  fsumiun  14534  sadeq  15175  bitsres  15176  smuval2  15185  smumul  15196  ressinbas  15917  lubdm  16960  glbdm  16973  sylow2a  18015  lsmmod2  18070  lsmdisj2r  18079  ablfac1eu  18453  ressmplbas2  19436  opsrtoslem1  19465  pjdm  20032  rintopn  20695  ordtrest2  20989  cmpsublem  21183  kgentopon  21322  hausdiag  21429  uzrest  21682  ufprim  21694  trust  22014  metnrmlem3  22645  clsocv  23030  ismbl  23275  unmbl  23286  volinun  23295  voliunlem1  23299  ovolioo  23317  itg2cnlem2  23510  ellimc2  23622  limcflf  23626  lhop1lem  23757  lgsquadlem3  25088  rplogsum  25197  umgrislfupgrlem  25998  spthispth  26603  0pth  26966  1pthdlem2  26976  frgrncvvdeqlem3  27145  ex-in  27252  chdmj3i  28312  chdmj4i  28313  chjassi  28315  pjoml2i  28414  pjoml3i  28415  cmcmlem  28420  cmcm2i  28422  cmbr3i  28429  fh3i  28452  fh4i  28453  osumcor2i  28473  mayetes3i  28558  mdslmd3i  29161  mdexchi  29164  atabsi  29230  dmdbr5ati  29251  inin  29324  uniin2  29340  ordtrest2NEW  29943  hasheuni  30121  carsgclctunlem1  30353  eulerpartgbij  30408  fiblem  30434  cvmscld  31229  msrid  31416  dfpo2  31620  elrn3  31628  noextend  31793  noextendseq  31794  madeval2  31910  bj-inrab3  32900  poimirlem15  33395  mblfinlem2  33418  ftc1anclem6  33461  pol0N  35014  mapfzcons2  37101  diophrw  37141  conrel2d  37775  iunrelexp0  37813  hashnzfz  38339  disjinfi  39196  fourierdlem80  40166  sge0resplit  40386  sge0split  40389  caragenuncllem  40489
  Copyright terms: Public domain W3C validator