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 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
Assertion prtlem13 ( 𝑧 ∼ 𝑤 ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) )

Proof

Step Hyp Ref Expression
1 prtlem13.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
2 vex ⊢ 𝑧 ∈ V
3 vex ⊢ 𝑤 ∈ V
4 elequ2 ⊢ ( 𝑢 = 𝑣 → ( 𝑥 ∈ 𝑢 ↔ 𝑥 ∈ 𝑣 ) )
5 elequ2 ⊢ ( 𝑢 = 𝑣 → ( 𝑦 ∈ 𝑢 ↔ 𝑦 ∈ 𝑣 ) )
6 4 5 anbi12d ⊢ ( 𝑢 = 𝑣 → ( ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) ↔ ( 𝑥 ∈ 𝑣 ∧ 𝑦 ∈ 𝑣 ) ) )
7 6 cbvrexvw ⊢ ( ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑥 ∈ 𝑣 ∧ 𝑦 ∈ 𝑣 ) )
8 elequ1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑣 ↔ 𝑧 ∈ 𝑣 ) )
9 elequ1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝑣 ↔ 𝑤 ∈ 𝑣 ) )
10 8 9 bi2anan9 ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ 𝑣 ∧ 𝑦 ∈ 𝑣 ) ↔ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
11 10 rexbidv ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ∃ 𝑣 ∈ 𝐴 ( 𝑥 ∈ 𝑣 ∧ 𝑦 ∈ 𝑣 ) ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
12 7 11 bitrid ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
13 2 3 12 1 braba ⊢ ( 𝑧 ∼ 𝑤 ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) )