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	⊢ ( ( 𝑅 ↾ { 𝐴 } ) ∈ 𝑉 → [ 𝐴 ] 𝑅 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		df-ec	⊢ [ 𝐴 ] 𝑅 = ( 𝑅 “ { 𝐴 } )
2		snex	⊢ { 𝐴 } ∈ V
3		imaexALTV	⊢ ( ( 𝑅 ∈ V ∨ ( ( 𝑅 ↾ { 𝐴 } ) ∈ 𝑉 ∧ { 𝐴 } ∈ V ) ) → ( 𝑅 “ { 𝐴 } ) ∈ V )
4	3	olcs	⊢ ( ( ( 𝑅 ↾ { 𝐴 } ) ∈ 𝑉 ∧ { 𝐴 } ∈ V ) → ( 𝑅 “ { 𝐴 } ) ∈ V )
5	2 4	mpan2	⊢ ( ( 𝑅 ↾ { 𝐴 } ) ∈ 𝑉 → ( 𝑅 “ { 𝐴 } ) ∈ V )
6	1 5	eqeltrid	⊢ ( ( 𝑅 ↾ { 𝐴 } ) ∈ 𝑉 → [ 𝐴 ] 𝑅 ∈ V )