Theorem dmuncnvepres

Description: Domain of the union with the converse epsilon, restricted. (Contributed by Peter Mazsa, 28-Jan-2026)

	Ref	Expression
Assertion	dmuncnvepres	⊢ dom ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) = ( 𝐴 ∩ ( dom 𝑅 ∪ ( V ∖ { ∅ } ) ) )

Proof

Step	Hyp	Ref	Expression
1		dmres	⊢ dom ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) = ( 𝐴 ∩ dom ( 𝑅 ∪ ◡ E ) )
2		dmun	⊢ dom ( 𝑅 ∪ ◡ E ) = ( dom 𝑅 ∪ dom ◡ E )
3		dmcnvep	⊢ dom ◡ E = ( V ∖ { ∅ } )
4	3	uneq2i	⊢ ( dom 𝑅 ∪ dom ◡ E ) = ( dom 𝑅 ∪ ( V ∖ { ∅ } ) )
5	2 4	eqtri	⊢ dom ( 𝑅 ∪ ◡ E ) = ( dom 𝑅 ∪ ( V ∖ { ∅ } ) )
6	5	ineq2i	⊢ ( 𝐴 ∩ dom ( 𝑅 ∪ ◡ E ) ) = ( 𝐴 ∩ ( dom 𝑅 ∪ ( V ∖ { ∅ } ) ) )
7	1 6	eqtri	⊢ dom ( ( 𝑅 ∪ ◡ E ) ↾ 𝐴 ) = ( 𝐴 ∩ ( dom 𝑅 ∪ ( V ∖ { ∅ } ) ) )