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

Theorem ineq12i 3370
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 3367 . 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 1625    i^i cin 3153
This theorem is referenced by:  undir  3420  difundi  3423  difindir  3426  inrab  3442  inrab2  3443  dfif4  3578  dfif5  3579  orduniss2  4626  inxp  4820  resindi  4973  resindir  4974  rnin  5092  funtp  5305  offres  6094  fodomr  7014  wemapwe  7402  explecnv  12325  psssdm2  14326  ablfacrp  15303  pjfval2  16611  iundisj2  18908  lejdiri  22120  cmbr3i  22181  nonbooli  22232  5oai  22242  3oalem5  22247  mayetes3i  22311  mdexchi  22917  xppreima  23213  xpinpreima  23292  xpinpreima2  23293  disjpreima  23363  iundisj2fi  23366  iundisj2f  23368  predin  24191  pprodcnveq  24425  dfiota3  24464  domncnt  25293  ranncnt  25294  dnwech  27156  fgraphopab  27540  onfrALTlem5  28363  onfrALTlem4  28364  onfrALTlem5VD  28734  onfrALTlem4VD  28735
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161
  Copyright terms: Public domain W3C validator