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

Theorem rexeq 3055
Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.)
Assertion
Ref Expression
rexeq
Distinct variable groups:   ,   ,

Proof of Theorem rexeq
StepHypRef Expression
1 nfcv 2619 . 2
2 nfcv 2619 . 2
31, 2rexeqf 3051 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  E.wrex 2808
This theorem is referenced by:  rexeqi  3059  rexeqdv  3061  rexeqbi1dv  3063  unieq  4257  exss  4715  qseq1  7380  1sdom  7742  pssnn  7758  indexfi  7848  supeq1  7925  bnd2  8332  dfac2  8532  cflem  8647  cflecard  8654  cfeq0  8657  cfsuc  8658  cfflb  8660  cofsmo  8670  elwina  9085  eltskg  9149  rankcf  9176  elnp  9386  elnpi  9387  genpv  9398  xrsupsslem  11527  xrinfmsslem  11528  xrsupss  11529  xrinfmss  11530  isdrs  15563  isipodrs  15791  neifval  19600  ishaus  19823  2ndc1stc  19952  1stcrest  19954  lly1stc  19997  isref  20010  islocfin  20018  tx1stc  20151  isust  20706  iscfilu  20791  met1stc  21024  iscfil  21704  isgrpo  25198  chne0  26412  pstmfval  27875  dya2iocuni  28254  nobndlem2  29453  nobndlem8  29459  altxpeq1  29623  altxpeq2  29624  elhf2  29832  cover2g  30205  indexdom  30225  istotbnd  30265  diophrex  30709  hbtlem1  31072  hbtlem7  31074  bj-sngleq  34525  pmapglb2xN  35496  paddval  35522  elpadd0  35533
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-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813
  Copyright terms: Public domain W3C validator