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

Theorem rexeqbi1dv 3067
 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:   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem rexeqbi1dv
StepHypRef Expression
1 rexeq 3059 . 2
2 raleqd.1 . . 3
32rexbidv 2973 . 2
41, 3bitrd 253 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wceq 1379  wrex 2815 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-ext 2445 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820 This theorem is referenced by:  fri  4841  frsn  5070  isofrlem  6224  f1oweALT  6768  frxp  6893  1sdom  7722  oieq2  7938  zfregcl  8020  ishaus  19617  isreg  19627  isnrm  19630  lebnumlem3  21226  1vwmgra  24707  3vfriswmgra  24709  isgrpo  24902  isexid2  25031  ismndo2  25051  rngomndo  25127  pjhth  26015  frmin  28927  stoweidlem28  31356  bnj1154  33152
 Copyright terms: Public domain W3C validator