Theorem cbvrexv 1334

Description: Change the bound variable of a restricted existential quantifier using implicit substitution.

Hypothesis

Ref	Expression
cbvralv.1	⊢ (x = y → (φ ↔ ψ))

Assertion

Ref	Expression
cbvrexv	⊢ (∃x ∈ A φ ↔ ∃y ∈ A ψ)

Distinct variable group(s):   φ,y   ψ,x   x,y,A

Proof of Theorem cbvrexv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 ⊢ (φ → ∀yφ)
2		ax-17 925	. 2 ⊢ (ψ → ∀xψ)
3		cbvralv.1	. 2 ⊢ (x = y → (φ ↔ ψ))
4	1, 2, 3	cbvrex 1332	1 ⊢ (∃x ∈ A φ ↔ ∃y ∈ A ψ)

Syntax hints:   → wi 2   ↔ wb 127   = weq 797  ∃wrex 1202

This theorem is referenced by:  cbviunv 2016  dffr2 2171  funcnvuni 2706  tfrlem3 2951  abianfp 3000  php3 3411  ominf 3423  pssnn 3428  ssfi 3430  unfi 3441  trcl 3489  r1pwcl 3530  aceq2 3554  aceq5lem4 3561  kmlem8 3587  kmlem14 3593  creur 4532  creui 4533  projlem15 5207  pjthu 5241  pjthu2 5242

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-8 798  ax-9 799  ax-12 802  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