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

Theorem ineq12i 3698
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 3695 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3mp2an 672 1  |-  ( A  i^i  C )  =  ( B  i^i  D
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    i^i cin 3475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483
This theorem is referenced by:  undir  3747  difundi  3750  difindir  3753  inrab  3770  inrab2  3771  dfif4  3954  dfif5  3955  inxp  5135  resindi  5289  resindir  5290  rnin  5415  inimass  5422  funtp  5640  orduniss2  6652  offres  6779  fodomr  7668  wemapwe  8139  wemapweOLD  8140  explecnv  13639  psssdm2  15702  ablfacrp  16919  pjfval2  18535  ofco2  18748  iundisj2  21722  lejdiri  26161  cmbr3i  26222  nonbooli  26273  5oai  26283  3oalem5  26288  mayetes3i  26352  mdexchi  26958  disjpreima  27146  disjxpin  27148  iundisj2f  27150  xppreima  27187  iundisj2fi  27298  xpinpreima  27552  xpinpreima2  27553  ordtcnvNEW  27566  predin  28874  pprodcnveq  29138  dfiota3  29178  ptrest  29653  ftc1anclem6  29700  dnwech  30626  fgraphopab  30803  onfrALTlem5  32412  onfrALTlem4  32413  onfrALTlem5VD  32783  onfrALTlem4VD  32784  bj-inrab  33594
  Copyright terms: Public domain W3C validator