Theorem rexeq1d 1836

Description: Equality deduction for restricted existential quantifier.

Hypothesis

Ref	Expression
raleq1d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
rexeq1d	⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ B ψ))

Distinct variable groups:   x,A   x,B

Proof of Theorem rexeq1d

Step	Hyp	Ref	Expression
1		raleq1d.1	. 2 ⊢ (φ → A = B)
2		rexeq1 1833	. 2 ⊢ (A = B → (∃x ∈ A ψ ↔ ∃x ∈ B ψ))
3	1, 2	syl 10	1 ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ B ψ))

Syntax hints:   → wi 3   ↔ wb 144   = wceq 992  ∃wrex 1692

This theorem is referenced by:  rexeq12d 1841  clmi2a 7294  opnfval 8067  cmsss 8208  hlcompl 8879  pjth 9510  pjtheu 9512  pjmval 9514  cayleythlem 10698  bwt2 11123  isplig 11319  compcov 11486  compsublem 11487  compsub 11488  uncomp 11490  hscptsscld 11491  cncomp 11494  alexsublem4 11499  alexsub 11500  islocfin 11567  locfinnei 11573  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  hausfillim 11685  filfm 11706  dirge 11754  totbndss 11993  heiborlem1 12011  heiborlem9 12019  heiborlem16 12026  heiborlem42 12052

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-cleq 1511  df-clel 1514  df-rex 1696

Copyright terms: Public domain