Theorem cnvepimaex

Description: The image of converse epsilon exists, proof via imaexALTV (see also cnvepima and uniexg for alternate way). (Contributed by Peter Mazsa, 22-Mar-2023)

	Ref	Expression
Assertion	cnvepimaex	⊢ ( 𝐴 ∈ 𝑉 → ( ◡ E “ 𝐴 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		cnvepresex	⊢ ( 𝐴 ∈ 𝑉 → ( ◡ E ↾ 𝐴 ) ∈ V )
2		imaexALTV	⊢ ( ( ◡ E ∈ V ∨ ( ( ◡ E ↾ 𝐴 ) ∈ V ∧ 𝐴 ∈ 𝑉 ) ) → ( ◡ E “ 𝐴 ) ∈ V )
3	2	olcs	⊢ ( ( ( ◡ E ↾ 𝐴 ) ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( ◡ E “ 𝐴 ) ∈ V )
4	1 3	mpancom	⊢ ( 𝐴 ∈ 𝑉 → ( ◡ E “ 𝐴 ) ∈ V )