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

Theorem ineq12 3648
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 3646 . 2  |-  ( A  =  B  ->  ( A  i^i  C )  =  ( B  i^i  C
) )
2 ineq2 3647 . 2  |-  ( C  =  D  ->  ( B  i^i  C )  =  ( B  i^i  D
) )
31, 2sylan9eq 2512 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  i^i  C
)  =  ( B  i^i  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370    i^i cin 3428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3073  df-in 3436
This theorem is referenced by:  ineq12i  3651  ineq12d  3654  ineqan12d  3655  fnun  5618  undifixp  7402  endisj  7501  sbthlem8  7531  fiin  7776  pm54.43  8274  kmlem9  8431  indistopon  18730  epttop  18738  restbas  18887  ordtbas2  18920  txbas  19265  ptbasin  19275  trfbas2  19541  snfil  19562  fbasrn  19582  trfil2  19585  fmfnfmlem3  19654  ustuqtop2  19942  minveclem3b  21040  isperp  23241  frrlem4  27908  diophin  29252  kelac2lem  29558
  Copyright terms: Public domain W3C validator