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

Theorem ineq12i 3541
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 3538 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3mp2an 655 1  |-  ( A  i^i  C )  =  ( B  i^i  D
)
Colors of variables: wff set class
Syntax hints:    = wceq 1653    i^i cin 3320
This theorem is referenced by:  undir  3591  difundi  3594  difindir  3597  inrab  3614  inrab2  3615  dfif4  3751  dfif5  3752  orduniss2  4814  inxp  5008  resindi  5163  resindir  5164  rnin  5282  inimass  5289  funtp  5504  offres  6320  fodomr  7259  wemapwe  7655  explecnv  12645  psssdm2  14648  ablfacrp  15625  pjfval2  16937  iundisj2  19444  lejdiri  23042  cmbr3i  23103  nonbooli  23154  5oai  23164  3oalem5  23169  mayetes3i  23233  mdexchi  23839  disjpreima  24027  disjxpin  24029  iundisj2f  24031  xppreima  24060  iundisj2fi  24154  xpinpreima  24305  xpinpreima2  24306  predin  25465  pprodcnveq  25729  dfiota3  25769  ftc1anclem6  26286  dnwech  27124  fgraphopab  27507  onfrALTlem5  28629  onfrALTlem4  28630  onfrALTlem5VD  28998  onfrALTlem4VD  28999
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2959  df-in 3328
  Copyright terms: Public domain W3C validator