MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ineq12i Structured version   Unicode version

Theorem ineq12i 3600
Description: Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
Hypotheses
Ref Expression
ineq1i.1  |-  A  =  B
ineq12i.2  |-  C  =  D
Assertion
Ref Expression
ineq12i  |-  ( A  i^i  C )  =  ( B  i^i  D
)

Proof of Theorem ineq12i
StepHypRef Expression
1 ineq1i.1 . 2  |-  A  =  B
2 ineq12i.2 . 2  |-  C  =  D
3 ineq12 3597 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3mp2an 676 1  |-  ( A  i^i  C )  =  ( B  i^i  D
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    i^i cin 3373
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-v 3019  df-in 3381
This theorem is referenced by:  undir  3660  difundi  3663  difindir  3666  inrab  3683  inrab2  3684  elneldisj  3725  dfif4  3864  dfif5  3865  inxp  4924  resindi  5077  resindir  5078  rnin  5202  inimass  5209  predin  5360  funtp  5591  orduniss2  6613  offres  6741  fodomr  7671  wemapwe  8149  cotr3  12981  explecnv  13861  psssdm2  16399  ablfacrp  17637  pjfval2  19209  ofco2  19413  iundisj2  22439  lejdiri  27129  cmbr3i  27190  nonbooli  27241  5oai  27251  3oalem5  27256  mayetes3i  27319  mdexchi  27925  disjpreima  28135  disjxpin  28139  iundisj2f  28141  xppreima  28189  iundisj2fi  28318  xpinpreima  28659  xpinpreima2  28660  ordtcnvNEW  28673  pprodcnveq  30594  dfiota3  30634  bj-inrab  31441  ptrest  31846  ftc1anclem6  31929  dnwech  35819  fgraphopab  36000  onfrALTlem5  36821  onfrALTlem4  36822  onfrALTlem5VD  37198  onfrALTlem4VD  37199  disjxp1  37327  disjinfi  37372
  Copyright terms: Public domain W3C validator