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

Metamath Proof Explorer

Theorem opabid2

Description: A relation expressed as an ordered pair abstraction. (Contributed by NM, 11-Dec-2006)

Ref Expression
Assertion opabid2 ⊢ Rel ⁡ A → x y | x y ∈ A = A

Proof

Step Hyp Ref Expression
1 vex ⊢ z ∈ V
2 vex ⊢ w ∈ V
3 opeq1 ⊢ x = z → x y = z y
4 3 eleq1d ⊢ x = z → x y ∈ A ↔ z y ∈ A
5 opeq2 ⊢ y = w → z y = z w
6 5 eleq1d ⊢ y = w → z y ∈ A ↔ z w ∈ A
7 1 2 4 6 opelopab ⊢ z w ∈ x y | x y ∈ A ↔ z w ∈ A
8 7 gen2 ⊢ ∀ z ∀ w z w ∈ x y | x y ∈ A ↔ z w ∈ A
9 relopabv ⊢ Rel ⁡ x y | x y ∈ A
10 eqrel ⊢ Rel ⁡ x y | x y ∈ A ∧ Rel ⁡ A → x y | x y ∈ A = A ↔ ∀ z ∀ w z w ∈ x y | x y ∈ A ↔ z w ∈ A
11 9 10 mpan ⊢ Rel ⁡ A → x y | x y ∈ A = A ↔ ∀ z ∀ w z w ∈ x y | x y ∈ A ↔ z w ∈ A
12 8 11 mpbiri ⊢ Rel ⁡ A → x y | x y ∈ A = A