Theorem rexeqdv 2270

Description: Equality deduction for restricted existential quantifier.

Hypothesis

Ref	Expression
raleq1d.1	|- (ph -> A = B)

Assertion

Ref	Expression
rexeqdv	|- (ph -> (E.x e. A ps <-> E.x e. B ps))

Distinct variable groups:   x,A   x,B

Proof of Theorem rexeqdv

Step	Hyp	Ref	Expression
1		raleq1d.1	. 2 |- (ph -> A = B)
2		rexeq 2267	. 2 |- (A = B -> (E.x e. A ps <-> E.x e. B ps))
3	1, 2	syl 12	1 |- (ph -> (E.x e. A ps <-> E.x e. B ps))

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298  E.wrex 2106

This theorem is referenced by:  rexeqbidv 2275  clmi2a 8351  opnfval 9134  cmsss 9275  hlcompl 9964  hausfillim 10303  cncomp 10331  isplig 10345  dirge 10357  pjth 10867  pjtheu 10869  pjmval 10871  cayleythlem 13645  fatesg 14293  bwt2 14960  isplibg1 15309  compcov 15429  compsublem 15430  compsub 15431  uncomp 15433  hscptsscld 15434  alexsublem4 15440  alexsub 15441  islocfin 15506  locfinnei 15512  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  filfm 15600  zornn0 15764  totbndss 15937  heiborlem1 15955  heiborlem9 15963  heiborlem16 15970  heiborlem42 15996  isgrpda 16033  pi1fval 16092  isdivrng2 16111  pointset 17222

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-cleq 1877  df-clel 1880  df-rex 2110

Copyright terms: Public domain