Metamath Proof Explorer

Theorem elisset

Description: An element of a class exists. (Contributed by NM, 1-May-1995) Reduce dependencies on axioms. (Revised by BJ, 29-Apr-2019)

Ref Expression
Assertion elisset ⊢ A ∈ V → ∃ x x = A

Proof

Step Hyp Ref Expression
1 elissetv ⊢ A ∈ V → ∃ y y = A
2 vextru ⊢ y ∈ z | ⊤
3 2 biantru ⊢ y = A ↔ y = A ∧ y ∈ z | ⊤
4 3 exbii ⊢ ∃ y y = A ↔ ∃ y y = A ∧ y ∈ z | ⊤
5 dfclel ⊢ A ∈ z | ⊤ ↔ ∃ y y = A ∧ y ∈ z | ⊤
6 4 5 bitr4i ⊢ ∃ y y = A ↔ A ∈ z | ⊤
7 vextru ⊢ x ∈ z | ⊤
8 7 biantru ⊢ x = A ↔ x = A ∧ x ∈ z | ⊤
9 8 exbii ⊢ ∃ x x = A ↔ ∃ x x = A ∧ x ∈ z | ⊤
10 dfclel ⊢ A ∈ z | ⊤ ↔ ∃ x x = A ∧ x ∈ z | ⊤
11 9 10 bitr4i ⊢ ∃ x x = A ↔ A ∈ z | ⊤
12 6 11 bitr4i ⊢ ∃ y y = A ↔ ∃ x x = A
13 1 12 sylib ⊢ A ∈ V → ∃ x x = A