Theorem dfcoels

Description: Alternate definition of the class of coelements on the class A . (Contributed by Peter Mazsa, 20-Apr-2019)

	Ref	Expression
Assertion	dfcoels	⊢ ∼ 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }

Proof

Step	Hyp	Ref	Expression
1		df-coels	⊢ ∼ 𝐴 = ≀ ( ◡ E ↾ 𝐴 )
2		1cossres	⊢ ≀ ( ◡ E ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑢 ◡ E 𝑥 ∧ 𝑢 ◡ E 𝑦 ) }
3		brcnvep	⊢ ( 𝑢 ∈ V → ( 𝑢 ◡ E 𝑥 ↔ 𝑥 ∈ 𝑢 ) )
4	3	elv	⊢ ( 𝑢 ◡ E 𝑥 ↔ 𝑥 ∈ 𝑢 )
5		brcnvep	⊢ ( 𝑢 ∈ V → ( 𝑢 ◡ E 𝑦 ↔ 𝑦 ∈ 𝑢 ) )
6	5	elv	⊢ ( 𝑢 ◡ E 𝑦 ↔ 𝑦 ∈ 𝑢 )
7	4 6	anbi12i	⊢ ( ( 𝑢 ◡ E 𝑥 ∧ 𝑢 ◡ E 𝑦 ) ↔ ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) )
8	7	rexbii	⊢ ( ∃ 𝑢 ∈ 𝐴 ( 𝑢 ◡ E 𝑥 ∧ 𝑢 ◡ E 𝑦 ) ↔ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) )
9	8	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑢 ◡ E 𝑥 ∧ 𝑢 ◡ E 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
10	1 2 9	3eqtri	⊢ ∼ 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }