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\upharpoonright }_{\left\{A\right\}}\in V\to \left[A\right]R\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-ec	$$⊢\left[A\right]R=R\left[\left\{A\right\}\right]$$
2		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
3		imaexALTV	$$⊢\left(R\in \mathrm{V}\vee \left({R\upharpoonright }_{\left\{A\right\}}\in V\wedge \left\{A\right\}\in \mathrm{V}\right)\right)\to R\left[\left\{A\right\}\right]\in \mathrm{V}$$
4	3	olcs	$$⊢\left({R\upharpoonright }_{\left\{A\right\}}\in V\wedge \left\{A\right\}\in \mathrm{V}\right)\to R\left[\left\{A\right\}\right]\in \mathrm{V}$$
5	2 4	mpan2	$$⊢{R\upharpoonright }_{\left\{A\right\}}\in V\to R\left[\left\{A\right\}\right]\in \mathrm{V}$$
6	1 5	eqeltrid	$$⊢{R\upharpoonright }_{\left\{A\right\}}\in V\to \left[A\right]R\in \mathrm{V}$$