This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvexsv

Description: A theorem pertaining to the substitution for an existentially quantified variable when the substituted variable does not occur in the quantified wff. (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cbvexsv ⊢ ∃ x φ ↔ ∃ y y x φ

Proof

Step Hyp Ref Expression
1 cbvrexsv ⊢ ∃ x ∈ V φ ↔ ∃ y ∈ V y x φ
2 rexv ⊢ ∃ x ∈ V φ ↔ ∃ x φ
3 rexv ⊢ ∃ y ∈ V y x φ ↔ ∃ y y x φ
4 1 2 3 3bitr3i ⊢ ∃ x φ ↔ ∃ y y x φ