Theorem rexeq 1325

Description: Equality theorem for restricted existential quantifier.

Assertion

Ref	Expression
rexeq	⊢ (A = B → (∃x ∈ A φ ↔ ∃x ∈ B φ))

Distinct variable group(s):   x,A   x,B

Proof of Theorem rexeq

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 ⊢ (y ∈ A → ∀x y ∈ A)
2		ax-17 925	. 2 ⊢ (y ∈ B → ∀x y ∈ B)
3	1, 2	rexeqf 1322	1 ⊢ (A = B → (∃x ∈ A φ ↔ ∃x ∈ B φ))

Syntax hints:   → wi 2   ↔ wb 127   = wceq 1091   ∈ wcel 1092  ∃wrex 1202

This theorem is referenced by:  rexeqd 1328  exss 1881  supeq1 2155  abrexexg 2913  qseq1 3225  pssnn 3428  bnd2 3549  aceq6b 3565  cflem 3700  cflecard 3707  cfsuc 3709  elnp 3886  genpv 3896  ch2 5149  pjtht 5240  pjthut 5243  pjmvalt 5245  pjpj0 5259  shsumvalt 5279  chne0t 5452

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-9 799  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-cleq 1097  df-clel 1099  df-rex 1206

metamath.org