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

Theorem ineq12 3365
Description: Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.)
Assertion
Ref Expression
ineq12  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )

Proof of Theorem ineq12
StepHypRef Expression
1 ineq1 3363 . 2  |-  ( A  =  B  ->  ( A  i^i  C )  =  ( B  i^i  C
) )
2 ineq2 3364 . 2  |-  ( C  =  D  ->  ( B  i^i  C )  =  ( B  i^i  D
) )
31, 2sylan9eq 2335 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    i^i cin 3151
This theorem is referenced by:  ineq12i  3368  ineq12d  3371  ineqan12d  3372  fnun  5350  undifixp  6852  endisj  6949  sbthlem8  6978  fiin  7175  pm54.43  7633  kmlem9  7784  indistopon  16738  epttop  16746  restbas  16889  ordtbas2  16921  txbas  17262  ptbasin  17272  trfbas2  17538  snfil  17559  fbasrn  17579  trfil2  17582  fmfnfmlem3  17651  minveclem3b  18792  frrlem4  24284  diophin  26852  kelac2lem  27162
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