This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elissetv

Description: An element of a class exists. Version of elisset with a disjoint variable condition on V , x , avoiding df-clab . Prefer its use over elisset when sufficient (for instance in usages where x is a dummy variable). (Contributed by BJ, 14-Sep-2019)

		Ref	Expression
	Assertion	elissetv	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dfclel	⊢ ( 𝐴 ∈ 𝑉 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝑉 ) )
2		exsimpl	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ 𝑉 ) → ∃ 𝑥 𝑥 = 𝐴 )
3	1 2	sylbi	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 )