Metamath Proof Explorer

Theorem cbvopab2davw

Description: Change the second bound variable in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025)

Ref Expression
Hypothesis cbvopab2davw.1 ⊢ φ ∧ y = z → ψ ↔ χ
Assertion cbvopab2davw ⊢ φ → x y | ψ = x z | χ

Proof

Step Hyp Ref Expression
1 cbvopab2davw.1 ⊢ φ ∧ y = z → ψ ↔ χ
2 opeq2 ⊢ y = z → x y = x z
3 2 eqeq2d ⊢ y = z → t = x y ↔ t = x z
4 3 adantl ⊢ φ ∧ y = z → t = x y ↔ t = x z
5 4 1 anbi12d ⊢ φ ∧ y = z → t = x y ∧ ψ ↔ t = x z ∧ χ
6 5 cbvexdvaw ⊢ φ → ∃ y t = x y ∧ ψ ↔ ∃ z t = x z ∧ χ
7 6 exbidv ⊢ φ → ∃ x ∃ y t = x y ∧ ψ ↔ ∃ x ∃ z t = x z ∧ χ
8 7 abbidv ⊢ φ → t | ∃ x ∃ y t = x y ∧ ψ = t | ∃ x ∃ z t = x z ∧ χ
9 df-opab ⊢ x y | ψ = t | ∃ x ∃ y t = x y ∧ ψ
10 df-opab ⊢ x z | χ = t | ∃ x ∃ z t = x z ∧ χ
11 8 9 10 3eqtr4g ⊢ φ → x y | ψ = x z | χ