Theorem dfcoss2

Description: Alternate definition of the class of cosets by R : x and y are cosets by R iff there exists a set u such that both x and y are are elements of the R -coset of u (see also the comment of dfec2 ). R is usually a relation. (Contributed by Peter Mazsa, 16-Jan-2018)

	Ref	Expression
Assertion	dfcoss2	⊢ ≀ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝑦 ∈ [ 𝑢 ] 𝑅 ) }

Proof

Step	Hyp	Ref	Expression
1		df-coss	⊢ ≀ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) }
2		elecALTV	⊢ ( ( 𝑢 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ [ 𝑢 ] 𝑅 ↔ 𝑢 𝑅 𝑥 ) )
3	2	el2v	⊢ ( 𝑥 ∈ [ 𝑢 ] 𝑅 ↔ 𝑢 𝑅 𝑥 )
4		elecALTV	⊢ ( ( 𝑢 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑦 ∈ [ 𝑢 ] 𝑅 ↔ 𝑢 𝑅 𝑦 ) )
5	4	el2v	⊢ ( 𝑦 ∈ [ 𝑢 ] 𝑅 ↔ 𝑢 𝑅 𝑦 )
6	3 5	anbi12i	⊢ ( ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝑦 ∈ [ 𝑢 ] 𝑅 ) ↔ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) )
7	6	exbii	⊢ ( ∃ 𝑢 ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝑦 ∈ [ 𝑢 ] 𝑅 ) ↔ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) )
8	7	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝑦 ∈ [ 𝑢 ] 𝑅 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) }
9	1 8	eqtr4i	⊢ ≀ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ 𝑦 ∈ [ 𝑢 ] 𝑅 ) }