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

Theorem rabeq 3103
Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.)
Assertion
Ref Expression
rabeq
Distinct variable groups:   ,   ,

Proof of Theorem rabeq
StepHypRef Expression
1 nfcv 2619 . 2
2 nfcv 2619 . 2
31, 2rabeqf 3102 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  {crab 2811
This theorem is referenced by:  rabeqbidv  3104  rabeqbidva  3105  difeq1  3614  ifeq1  3945  ifeq2  3946  rabsnif  4099  elfvmptrab  5977  supp0  6923  suppvalfn  6925  suppsnop  6932  fnsuppres  6946  pmvalg  7450  supeq2  7928  oieq2  7959  cantnffval  8101  scott0  8325  hsmex2  8834  iooval2  11591  fzval2  11704  hashbc  12502  elovmpt2wrd  12583  dfphi2  14304  phimullem  14309  mrcfval  15005  mrisval  15027  ipoval  15784  pmtrfval  16475  psgnfval  16525  pmtrsn  16544  lspfval  17619  lsppropd  17664  rrgval  17935  aspval  17977  psrval  18011  mvrfval  18076  ltbval  18136  opsrval  18139  dsmmbas2  18768  dsmmelbas  18770  frlmbas  18786  frlmbasOLD  18787  m1detdiag  19099  clsfval  19526  ordtrest  19703  ordtrest2lem  19704  ordtrest2  19705  isptfin  20017  islocfin  20018  xkoval  20088  xkopt  20156  qtopres  20199  kqval  20227  tsmsval2  20628  cncfval  21392  isphtpy  21481  cfilfval  21703  iscmet  21723  ttgval  24178  eengv  24282  isumgra  24315  isuslgra  24343  isusgra  24344  edgss  24352  wwlkn  24682  clwwlkn  24767  clwwlknprop  24772  hashecclwwlkn1  24834  usghashecclwwlk  24835  rusgrasn  24945  numclwwlkovf2  25084  numclwwlkqhash  25100  ordtprsval  27900  ordtrestNEW  27903  ordtrest2NEWlem  27904  omsval  28264  orrvcval4  28403  orrvcoel  28404  orrvccel  28405  snmlfval  28775  funray  29790  fvray  29791  itg2addnclem2  30067  cntotbnd  30292  pellfundval  30816  elmnc  31085  rgspnval  31117  rabeqd  31438  dvnprodlem1  31743  dvnprodlem2  31744  dvnprodlem3  31745  dvnprod  31746  isfusgra  32424  usgfis  32446  usgfisALT  32450  assintopmap  32530  rmsuppss  32963  mndpsuppss  32964  scmsuppss  32965  dmatALTval  33001  dmatALTbas  33002  docaffvalN  36848  docafvalN  36849  lcfr  37312  hlhilocv  37687
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-rab 2816
  Copyright terms: Public domain W3C validator