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

Metamath Proof Explorer

Theorem dfoprab3

Description: Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008)

Ref Expression
Hypothesis dfoprab3.1 ⊢ w = x y → φ ↔ ψ
Assertion dfoprab3 ⊢ w z | w ∈ V × V ∧ φ = x y z | ψ

Proof

Step Hyp Ref Expression
1 dfoprab3.1 ⊢ w = x y → φ ↔ ψ
2 dfoprab3s ⊢ x y z | ψ = w z | w ∈ V × V ∧ [˙ 1 st ⁡ w / x]˙ [˙ 2 nd ⁡ w / y]˙ ψ
3 fvex ⊢ 1 st ⁡ w ∈ V
4 fvex ⊢ 2 nd ⁡ w ∈ V
5 eqcom ⊢ x = 1 st ⁡ w ↔ 1 st ⁡ w = x
6 eqcom ⊢ y = 2 nd ⁡ w ↔ 2 nd ⁡ w = y
7 5 6 anbi12i ⊢ x = 1 st ⁡ w ∧ y = 2 nd ⁡ w ↔ 1 st ⁡ w = x ∧ 2 nd ⁡ w = y
8 eqopi ⊢ w ∈ V × V ∧ 1 st ⁡ w = x ∧ 2 nd ⁡ w = y → w = x y
9 7 8 sylan2b ⊢ w ∈ V × V ∧ x = 1 st ⁡ w ∧ y = 2 nd ⁡ w → w = x y
10 9 1 syl ⊢ w ∈ V × V ∧ x = 1 st ⁡ w ∧ y = 2 nd ⁡ w → φ ↔ ψ
11 10 bicomd ⊢ w ∈ V × V ∧ x = 1 st ⁡ w ∧ y = 2 nd ⁡ w → ψ ↔ φ
12 11 ex ⊢ w ∈ V × V → x = 1 st ⁡ w ∧ y = 2 nd ⁡ w → ψ ↔ φ
13 3 4 12 sbc2iedv ⊢ w ∈ V × V → [˙ 1 st ⁡ w / x]˙ [˙ 2 nd ⁡ w / y]˙ ψ ↔ φ
14 13 pm5.32i ⊢ w ∈ V × V ∧ [˙ 1 st ⁡ w / x]˙ [˙ 2 nd ⁡ w / y]˙ ψ ↔ w ∈ V × V ∧ φ
15 14 opabbii ⊢ w z | w ∈ V × V ∧ [˙ 1 st ⁡ w / x]˙ [˙ 2 nd ⁡ w / y]˙ ψ = w z | w ∈ V × V ∧ φ
16 2 15 eqtr2i ⊢ w z | w ∈ V × V ∧ φ = x y z | ψ