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	⊢ ( 𝑧 ∼ 𝑤 ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) )