Theorem ecxrncnvep

Description: The ( R |X.`' _E ) ` -coset of a set. (Contributed by Peter Mazsa, 22-May-2021)

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

Proof

Step	Hyp	Ref	Expression
1		ecxrn	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ( 𝑅 ⋉ ◡ E ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 ◡ E 𝑧 ) } )
2		brcnvep	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ◡ E 𝑧 ↔ 𝑧 ∈ 𝐴 ) )
3	2	anbi1cd	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 𝑅 𝑦 ∧ 𝐴 ◡ E 𝑧 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝐴 𝑅 𝑦 ) ) )
4	3	opabbidv	⊢ ( 𝐴 ∈ 𝑉 → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 ◡ E 𝑧 ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑧 ∈ 𝐴 ∧ 𝐴 𝑅 𝑦 ) } )
5	1 4	eqtrd	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ( 𝑅 ⋉ ◡ E ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑧 ∈ 𝐴 ∧ 𝐴 𝑅 𝑦 ) } )