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

Theorem ineq12i 3532
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 3529 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
41, 2, 3mp2an 654 1  |-  ( A  i^i  C )  =  ( B  i^i  D
)
Colors of variables: wff set class
Syntax hints:    = wceq 1652    i^i cin 3311
This theorem is referenced by:  undir  3582  difundi  3585  difindir  3588  inrab  3605  inrab2  3606  dfif4  3742  dfif5  3743  orduniss2  4804  inxp  4998  resindi  5153  resindir  5154  rnin  5272  inimass  5279  funtp  5494  offres  6310  fodomr  7249  wemapwe  7643  explecnv  12632  psssdm2  14635  ablfacrp  15612  pjfval2  16924  iundisj2  19431  lejdiri  23029  cmbr3i  23090  nonbooli  23141  5oai  23151  3oalem5  23156  mayetes3i  23220  mdexchi  23826  disjpreima  24014  disjxpin  24016  iundisj2f  24018  xppreima  24047  iundisj2fi  24141  xpinpreima  24292  xpinpreima2  24293  predin  25444  pprodcnveq  25678  dfiota3  25718  dnwech  27060  fgraphopab  27444  onfrALTlem5  28483  onfrALTlem4  28484  onfrALTlem5VD  28851  onfrALTlem4VD  28852
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319
  Copyright terms: Public domain W3C validator