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

Theorem ineq12i 3368
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 3365 . 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 3151
This theorem is referenced by:  undir  3418  difundi  3421  difindir  3424  inrab  3440  inrab2  3441  dfif4  3576  dfif5  3577  orduniss2  4624  inxp  4818  resindi  4971  resindir  4972  rnin  5090  funtp  5303  offres  6092  fodomr  7012  wemapwe  7400  explecnv  12323  psssdm2  14324  ablfacrp  15301  pjfval2  16609  iundisj2  18906  lejdiri  22118  cmbr3i  22179  nonbooli  22230  5oai  22240  3oalem5  22245  mayetes3i  22309  mdexchi  22915  xppreima  23211  xpinpreima  23290  xpinpreima2  23291  disjpreima  23361  iundisj2fi  23364  iundisj2f  23366  predin  24189  pprodcnveq  24423  dfiota3  24462  domncnt  25282  ranncnt  25283  dnwech  27145  fgraphopab  27529  onfrALTlem5  28307  onfrALTlem4  28308  onfrALTlem5VD  28661  onfrALTlem4VD  28662
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 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
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 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159
  Copyright terms: Public domain W3C validator