Theorem ecuncnvepres

Description: The restricted union with converse epsilon relation coset of B . (Contributed by Peter Mazsa, 28-Jan-2026)

	Ref	Expression
Assertion	ecuncnvepres	⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) = ( 𝐵 ∪ [ 𝐵 ] 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		ecunres	⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) = ( [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) ∪ [ 𝐵 ] ( ◡ E ↾ 𝐴 ) ) )
2		elecreseq	⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) = [ 𝐵 ] 𝑅 )
3		eccnvepres2	⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] ( ◡ E ↾ 𝐴 ) = 𝐵 )
4	2 3	uneq12d	⊢ ( 𝐵 ∈ 𝐴 → ( [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) ∪ [ 𝐵 ] ( ◡ E ↾ 𝐴 ) ) = ( [ 𝐵 ] 𝑅 ∪ 𝐵 ) )
5	1 4	eqtrd	⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) = ( [ 𝐵 ] 𝑅 ∪ 𝐵 ) )
6		uncom	⊢ ( [ 𝐵 ] 𝑅 ∪ 𝐵 ) = ( 𝐵 ∪ [ 𝐵 ] 𝑅 )
7	5 6	eqtrdi	⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) = ( 𝐵 ∪ [ 𝐵 ] 𝑅 ) )