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

Theorem ineq12i 3381
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 3378 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3mp2an 653 1  |-  ( A  i^i  C )  =  ( B  i^i  D
)
Colors of variables: wff set class
Syntax hints:    = wceq 1632    i^i cin 3164
This theorem is referenced by:  undir  3431  difundi  3434  difindir  3437  inrab  3453  inrab2  3454  dfif4  3589  dfif5  3590  orduniss2  4640  inxp  4834  resindi  4987  resindir  4988  rnin  5106  funtp  5319  offres  6108  fodomr  7028  wemapwe  7416  explecnv  12339  psssdm2  14340  ablfacrp  15317  pjfval2  16625  iundisj2  18922  lejdiri  22134  cmbr3i  22195  nonbooli  22246  5oai  22256  3oalem5  22261  mayetes3i  22325  mdexchi  22931  xppreima  23226  xpinpreima  23305  xpinpreima2  23306  disjpreima  23376  iundisj2fi  23379  iundisj2f  23381  predin  24260  pprodcnveq  24494  dfiota3  24533  domncnt  25385  ranncnt  25386  dnwech  27248  fgraphopab  27632  onfrALTlem5  28606  onfrALTlem4  28607  onfrALTlem5VD  28977  onfrALTlem4VD  28978
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172
  Copyright terms: Public domain W3C validator