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

Theorem ineq12 3677
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 3675 . 2  |-  ( A  =  B  ->  ( A  i^i  C )  =  ( B  i^i  C
) )
2 ineq2 3676 . 2  |-  ( C  =  D  ->  ( B  i^i  C )  =  ( B  i^i  D
) )
31, 2sylan9eq 2502 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 1381    i^i cin 3457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-in 3465
This theorem is referenced by:  ineq12i  3680  ineq12d  3683  ineqan12d  3684  fnun  5673  undifixp  7503  endisj  7602  sbthlem8  7632  fiin  7880  pm54.43  8379  kmlem9  8536  indistopon  19368  epttop  19376  restbas  19525  ordtbas2  19558  txbas  19934  ptbasin  19944  trfbas2  20210  snfil  20231  fbasrn  20251  trfil2  20254  fmfnfmlem3  20323  ustuqtop2  20611  minveclem3b  21709  isperp  23954  frrlem4  29358  diophin  30674  kelac2lem  30978
  Copyright terms: Public domain W3C validator