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

Theorem ineq12i 3456
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 3453 . 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 1647    i^i cin 3237
This theorem is referenced by:  undir  3506  difundi  3509  difindir  3512  inrab  3528  inrab2  3529  dfif4  3665  dfif5  3666  orduniss2  4727  inxp  4921  resindi  5074  resindir  5075  rnin  5193  funtp  5407  offres  6219  fodomr  7155  wemapwe  7547  explecnv  12531  psssdm2  14534  ablfacrp  15511  pjfval2  16826  iundisj2  19121  lejdiri  22431  cmbr3i  22492  nonbooli  22543  5oai  22553  3oalem5  22558  mayetes3i  22622  mdexchi  23228  disjpreima  23424  iundisj2f  23427  inimass  23433  xppreima  23461  iundisj2fi  23556  xpinpreima  23659  xpinpreima2  23660  predin  24930  pprodcnveq  25164  dfiota3  25203  dnwech  26651  fgraphopab  27035  onfrALTlem5  28054  onfrALTlem4  28055  onfrALTlem5VD  28425  onfrALTlem4VD  28426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-in 3245
  Copyright terms: Public domain W3C validator