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

Theorem rexeq 3005
Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.)
Assertion
Ref Expression
rexeq  |-  ( A  =  B  ->  ( E. x  e.  A  ph  <->  E. x  e.  B  ph ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem rexeq
StepHypRef Expression
1 nfcv 2564 . 2  |-  F/_ x A
2 nfcv 2564 . 2  |-  F/_ x B
31, 2rexeqf 3001 1  |-  ( A  =  B  ->  ( E. x  e.  A  ph  <->  E. x  e.  B  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1405   E.wrex 2755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rex 2760
This theorem is referenced by:  rexeqi  3009  rexeqdv  3011  rexeqbi1dv  3013  unieq  4199  exss  4654  qseq1  7398  1sdom  7758  pssnn  7773  indexfi  7862  supeq1  7938  bnd2  8343  dfac2  8543  cflem  8658  cflecard  8665  cfeq0  8668  cfsuc  8669  cfflb  8671  cofsmo  8681  elwina  9094  eltskg  9158  rankcf  9185  elnp  9395  elnpi  9396  genpv  9407  xrsupsslem  11551  xrinfmsslem  11552  xrsupss  11553  xrinfmss  11554  isdrs  15887  isipodrs  16115  neifval  19893  ishaus  20116  2ndc1stc  20244  1stcrest  20246  lly1stc  20289  isref  20302  islocfin  20310  tx1stc  20443  isust  20998  iscfilu  21083  met1stc  21316  iscfil  21996  isgrpo  25612  chne0  26826  pstmfval  28328  dya2iocuni  28731  nobndlem2  30153  nobndlem8  30159  altxpeq1  30311  altxpeq2  30312  elhf2  30513  bj-sngleq  31090  cover2g  31487  indexdom  31507  istotbnd  31547  pmapglb2xN  32789  paddval  32815  elpadd0  32826  diophrex  35070  hbtlem1  35436  hbtlem7  35438
  Copyright terms: Public domain W3C validator