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

Theorem ineq12 3694
 Description: Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.)
Assertion
Ref Expression
ineq12

Proof of Theorem ineq12
StepHypRef Expression
1 ineq1 3692 . 2
2 ineq2 3693 . 2
31, 2sylan9eq 2518 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  i^icin 3474 This theorem is referenced by:  ineq12i  3697  ineq12d  3700  ineqan12d  3701  fnun  5692  undifixp  7525  endisj  7624  sbthlem8  7654  fiin  7902  pm54.43  8402  kmlem9  8559  indistopon  19502  epttop  19510  restbas  19659  ordtbas2  19692  txbas  20068  ptbasin  20078  trfbas2  20344  snfil  20365  fbasrn  20385  trfil2  20388  fmfnfmlem3  20457  ustuqtop2  20745  minveclem3b  21843  isperp  24089  frrlem4  29390  diophin  30706  kelac2lem  31010 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482
 Copyright terms: Public domain W3C validator