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

Theorem ineq12i 3369
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 3366 . 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 1623    i^i cin 3152
This theorem is referenced by:  undir  3419  difundi  3422  difindir  3425  inrab  3441  inrab2  3442  dfif4  3577  dfif5  3578  orduniss2  4623  inxp  4817  resindi  4970  resindir  4971  rnin  5089  funtp  5269  offres  6054  fodomr  7008  wemapwe  7396  explecnv  12319  psssdm2  14320  ablfacrp  15297  pjfval2  16605  iundisj2  18902  lejdiri  22114  cmbr3i  22175  nonbooli  22226  5oai  22236  3oalem5  22241  mayetes3i  22305  mdexchi  22911  predin  23593  pprodcnveq  23834  dfiota3  23872  domncnt  24693  ranncnt  24694  dnwech  26556  fgraphopab  26940  onfrALTlem5  27590  onfrALTlem4  27591  onfrALTlem5VD  27941  onfrALTlem4VD  27942
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160
  Copyright terms: Public domain W3C validator