Theorem ecxrn

Description: The ( R |X. S ) -coset of A . (Contributed by Peter Mazsa, 18-Apr-2020) (Revised by Peter Mazsa, 21-Sep-2021)

	Ref	Expression
Assertion	ecxrn	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) } )

Proof

Step	Hyp	Ref	Expression
1		elecxrn	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ) )
2		3anass	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ) )
3	2	2exbii	⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ) )
4	1 3	bitrdi	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ) ) )
5		elopab	⊢ ( 𝑥 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) } ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) ) )
6	4 5	bitr4di	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ↔ 𝑥 ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) } ) )
7	6	eqrdv	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) } )