Theorem ecexALTV

Description: Existence of a coset, like ecexg but with a weaker antecedent: only the restricion of R by the singleton of A needs to be a set, not R itself, see e.g. eccnvepex . (Contributed by Peter Mazsa, 22-Feb-2023)

	Ref	Expression
Assertion	ecexALTV	|- ( ( R |` { A } ) e. V -> [ A ] R e. _V )

Proof

Step	Hyp	Ref	Expression
1		df-ec	|- [ A ] R = ( R " { A } )
2		snex	|- { A } e. _V
3		imaexALTV	|- ( ( R e. _V \/ ( ( R |` { A } ) e. V /\ { A } e. _V ) ) -> ( R " { A } ) e. _V )
4	3	olcs	|- ( ( ( R |` { A } ) e. V /\ { A } e. _V ) -> ( R " { A } ) e. _V )
5	2 4	mpan2	|- ( ( R |` { A } ) e. V -> ( R " { A } ) e. _V )
6	1 5	eqeltrid	|- ( ( R |` { A } ) e. V -> [ A ] R e. _V )