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

Theorem rexeqbi1dv 3063
 Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.)
Hypothesis
Ref Expression
raleqd.1
Assertion
Ref Expression
rexeqbi1dv
Distinct variable groups:   ,   ,

Proof of Theorem rexeqbi1dv
StepHypRef Expression
1 rexeq 3055 . 2
2 raleqd.1 . . 3
32rexbidv 2968 . 2
41, 3bitrd 253 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  E.wrex 2808 This theorem is referenced by:  fri  4846  frsn  5075  isofrlem  6236  f1oweALT  6784  frxp  6910  1sdom  7742  oieq2  7959  zfregcl  8041  ishaus  19823  isreg  19833  isnrm  19836  lebnumlem3  21463  1vwmgra  25003  3vfriswmgra  25005  isgrpo  25198  isexid2  25327  ismndo2  25347  rngomndo  25423  pjhth  26311  frmin  29322  stoweidlem28  31810  bnj1154  34055 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