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

Theorem ineq2 4018
Description: Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
Assertion
Ref Expression
ineq2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem ineq2
StepHypRef Expression
1 ineq1 4017 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
2 incom 4015 . 2 (𝐶𝐴) = (𝐴𝐶)
3 incom 4015 . 2 (𝐶𝐵) = (𝐵𝐶)
41, 2, 33eqtr4g 2876 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  cin 3779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-in 3787
This theorem is referenced by:  ineq12  4019  ineq2i  4021  ineq2d  4024  uneqin  4091  intprg  4714  wefrc  5318  onfr  5989  onnseq  7687  qsdisj  8069  disjenex  8367  fiint  8486  elfiun  8585  dffi3  8586  cplem2  9010  dfac5  9244  kmlem2  9268  kmlem13  9279  kmlem14  9280  ackbij1lem16  9352  fin23lem12  9448  fin23lem19  9453  fin23lem33  9462  uzin2  14327  pgpfac1lem3  18698  pgpfac1lem5  18700  pgpfac1  18701  inopn  20938  basis1  20989  basis2  20990  baspartn  20993  fctop  21043  cctop  21045  ordtbaslem  21227  hausnei2  21392  cnhaus  21393  nrmsep  21396  isnrm2  21397  dishaus  21421  ordthauslem  21422  dfconn2  21457  nconnsubb  21461  finlocfin  21558  dissnlocfin  21567  locfindis  21568  kgeni  21575  pthaus  21676  txhaus  21685  xkohaus  21691  regr1lem  21777  fbasssin  21874  fbun  21878  fbunfip  21907  filconn  21921  isufil2  21946  ufileu  21957  filufint  21958  fmfnfmlem4  21995  fmfnfm  21996  fclsopni  22053  fclsbas  22059  fclsrest  22062  isfcf  22072  tsmsfbas  22165  ustincl  22245  ust0  22257  metreslem  22401  methaus  22559  qtopbaslem  22796  metnrmlem3  22898  ismbl  23530  shincl  28591  chincl  28709  chdmm1  28735  ledi  28750  cmbr  28794  cmbr3i  28810  cmbr3  28818  pjoml2  28821  stcltrlem1  29486  mdbr  29504  dmdbr  29509  cvmd  29546  cvexch  29584  sumdmdii  29625  mddmdin0i  29641  ofpreima2  29816  crefeq  30260  ldgenpisyslem1  30574  ldgenpisys  30577  inelsros  30589  diffiunisros  30590  elcarsg  30715  carsgclctunlem2  30729  carsgclctun  30731  ballotlemfval  30899  ballotlemgval  30933  cvmscbv  31585  cvmsdisj  31597  cvmsss2  31601  nepss  31943  tailfb  32715  bj-0int  33385  mblfinlem2  33779  lshpinN  34788  elrfi  37777  fipjust  38388  conrel1d  38473  ntrk0kbimka  38855  clsk3nimkb  38856  isotone2  38865  ntrclskb  38885  ntrclsk3  38886  ntrclsk13  38887  csbresgVD  39643  disjf1  39876  qinioo  40260  fouriersw  40945  nnfoctbdjlem  41169  meadjun  41176  caragenel  41209
  Copyright terms: Public domain W3C validator