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

Theorem ineq12i 3680
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 3677 . 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 1381    i^i cin 3457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-in 3465
This theorem is referenced by:  undir  3729  difundi  3732  difindir  3735  inrab  3752  inrab2  3753  dfif4  3937  dfif5  3938  inxp  5121  resindi  5275  resindir  5276  rnin  5401  inimass  5408  funtp  5626  orduniss2  6649  offres  6776  fodomr  7666  wemapwe  8137  wemapweOLD  8138  explecnv  13650  psssdm2  15714  ablfacrp  16985  pjfval2  18607  ofco2  18820  iundisj2  21825  lejdiri  26322  cmbr3i  26383  nonbooli  26434  5oai  26444  3oalem5  26449  mayetes3i  26513  mdexchi  27119  disjpreima  27310  disjxpin  27312  iundisj2f  27314  xppreima  27352  iundisj2fi  27467  xpinpreima  27754  xpinpreima2  27755  ordtcnvNEW  27768  predin  29237  pprodcnveq  29501  dfiota3  29541  ptrest  30016  ftc1anclem6  30063  dnwech  30962  fgraphopab  31139  onfrALTlem5  33022  onfrALTlem4  33023  onfrALTlem5VD  33393  onfrALTlem4VD  33394  bj-inrab  34207  cotr3  37443
  Copyright terms: Public domain W3C validator