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

Theorem eqeq12 2476
Description: Equality relationship among 4 classes. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
eqeq12

Proof of Theorem eqeq12
StepHypRef Expression
1 eqeq1 2461 . 2
2 eqeq2 2472 . 2
31, 2sylan9bb 699 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395
This theorem is referenced by:  eqeq12iOLD  2478  eqeq12d  2479  eqeqan12dOLD  2481  funopg  5625  eqfnfv  5981  soxp  6913  tfr3  7087  xpdom2  7632  dfac5lem4  8528  kmlem9  8559  sornom  8678  zorn2lem6  8902  elwina  9085  elina  9086  uzindOLD  10982  bcn1  12391  summo  13539  prodmo  13743  xpnnenOLD  13943  vdwlem12  14510  pslem  15836  gaorb  16345  gsumval3eu  16907  cygznlem3  18608  mat1ov  18950  dmatmulcl  19002  scmatscmiddistr  19010  scmatscm  19015  1mavmul  19050  chmatval  19330  dscmet  21093  dscopn  21094  iundisj2  21959  usgra2wlkspthlem2  24620  constr3trllem2  24651  frg2wot1  25057  frg2woteqm  25059  rngoridfz  25437  iundisj2f  27449  iundisj2fi  27602  erdszelem9  28643  fununiq  29200  sltval2  29416  nofulllem5  29466  unirep  30203  2f1fvneq  32307  csbfv12gALTVD  33699  bj-elid  34599
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-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449
  Copyright terms: Public domain W3C validator