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

Metamath Proof Explorer

Theorem prtlem13

Description: Lemma for prter1 , prter2 , prter3 and prtex . (Contributed by Rodolfo Medina, 13-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypothesis prtlem13.1 ⊢ ∼ ˙ = x y | ∃ u ∈ A x ∈ u ∧ y ∈ u
Assertion prtlem13 ⊢ z ∼ ˙ w ↔ ∃ v ∈ A z ∈ v ∧ w ∈ v

Proof

Step Hyp Ref Expression
1 prtlem13.1 ⊢ ∼ ˙ = x y | ∃ u ∈ A x ∈ u ∧ y ∈ u
2 vex ⊢ z ∈ V
3 vex ⊢ w ∈ V
4 elequ2 ⊢ u = v → x ∈ u ↔ x ∈ v
5 elequ2 ⊢ u = v → y ∈ u ↔ y ∈ v
6 4 5 anbi12d ⊢ u = v → x ∈ u ∧ y ∈ u ↔ x ∈ v ∧ y ∈ v
7 6 cbvrexvw ⊢ ∃ u ∈ A x ∈ u ∧ y ∈ u ↔ ∃ v ∈ A x ∈ v ∧ y ∈ v
8 elequ1 ⊢ x = z → x ∈ v ↔ z ∈ v
9 elequ1 ⊢ y = w → y ∈ v ↔ w ∈ v
10 8 9 bi2anan9 ⊢ x = z ∧ y = w → x ∈ v ∧ y ∈ v ↔ z ∈ v ∧ w ∈ v
11 10 rexbidv ⊢ x = z ∧ y = w → ∃ v ∈ A x ∈ v ∧ y ∈ v ↔ ∃ v ∈ A z ∈ v ∧ w ∈ v
12 7 11 bitrid ⊢ x = z ∧ y = w → ∃ u ∈ A x ∈ u ∧ y ∈ u ↔ ∃ v ∈ A z ∈ v ∧ w ∈ v
13 2 3 12 1 braba ⊢ z ∼ ˙ w ↔ ∃ v ∈ A z ∈ v ∧ w ∈ v