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

Theorem ineq12i 3684
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 3681 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3mp2an 670 1  |-  ( A  i^i  C )  =  ( B  i^i  D
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398    i^i cin 3460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468
This theorem is referenced by:  undir  3744  difundi  3747  difindir  3750  inrab  3767  inrab2  3768  dfif4  3944  dfif5  3945  inxp  5124  resindi  5277  resindir  5278  rnin  5400  inimass  5407  funtp  5622  orduniss2  6641  offres  6768  fodomr  7661  wemapwe  8130  wemapweOLD  8131  cotr3  12896  explecnv  13758  psssdm2  16044  ablfacrp  17312  pjfval2  18913  ofco2  19120  iundisj2  22125  lejdiri  26655  cmbr3i  26716  nonbooli  26767  5oai  26777  3oalem5  26782  mayetes3i  26846  mdexchi  27452  disjpreima  27655  disjxpin  27658  iundisj2f  27660  xppreima  27708  iundisj2fi  27836  xpinpreima  28123  xpinpreima2  28124  ordtcnvNEW  28137  predin  29509  pprodcnveq  29761  dfiota3  29801  ptrest  30288  ftc1anclem6  30335  dnwech  31233  fgraphopab  31411  onfrALTlem5  33708  onfrALTlem4  33709  onfrALTlem5VD  34086  onfrALTlem4VD  34087  bj-inrab  34896
  Copyright terms: Public domain W3C validator