Metamath Proof Explorer

Theorem bj-snglc

Description: Characterization of the elements of A in terms of elements of its singletonization. (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-snglc ⊢ A ∈ B ↔ A ∈ sngl B

Proof

Step Hyp Ref Expression
1 df-rex ⊢ ∃ x ∈ B A = x ↔ ∃ x x ∈ B ∧ A = x
2 bj-elsngl ⊢ A ∈ sngl B ↔ ∃ x ∈ B A = x
3 elisset ⊢ A ∈ B → ∃ x x = A
4 3 pm4.71i ⊢ A ∈ B ↔ A ∈ B ∧ ∃ x x = A
5 19.42v ⊢ ∃ x A ∈ B ∧ x = A ↔ A ∈ B ∧ ∃ x x = A
6 eleq1 ⊢ A = x → A ∈ B ↔ x ∈ B
7 6 eqcoms ⊢ x = A → A ∈ B ↔ x ∈ B
8 7 pm5.32ri ⊢ A ∈ B ∧ x = A ↔ x ∈ B ∧ x = A
9 8 exbii ⊢ ∃ x A ∈ B ∧ x = A ↔ ∃ x x ∈ B ∧ x = A
10 4 5 9 3bitr2i ⊢ A ∈ B ↔ ∃ x x ∈ B ∧ x = A
11 sneqbg ⊢ x ∈ V → x = A ↔ x = A
12 11 elv ⊢ x = A ↔ x = A
13 eqcom ⊢ x = A ↔ A = x
14 12 13 bitr3i ⊢ x = A ↔ A = x
15 14 anbi2i ⊢ x ∈ B ∧ x = A ↔ x ∈ B ∧ A = x
16 15 exbii ⊢ ∃ x x ∈ B ∧ x = A ↔ ∃ x x ∈ B ∧ A = x
17 10 16 bitri ⊢ A ∈ B ↔ ∃ x x ∈ B ∧ A = x
18 1 2 17 3bitr4ri ⊢ A ∈ B ↔ A ∈ sngl B