Metamath Proof Explorer

Theorem bj-snsetex

Description: The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep . (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-snsetex ⊢ A ∈ V → x | x ∈ A ∈ V

Proof

Step Hyp Ref Expression
1 elisset ⊢ A ∈ V → ∃ y y = A
2 eleq2 ⊢ y = A → x ∈ y ↔ x ∈ A
3 2 abbidv ⊢ y = A → x | x ∈ y = x | x ∈ A
4 eleq1 ⊢ x | x ∈ y = x | x ∈ A → x | x ∈ y ∈ V ↔ x | x ∈ A ∈ V
5 4 biimpd ⊢ x | x ∈ y = x | x ∈ A → x | x ∈ y ∈ V → x | x ∈ A ∈ V
6 3 5 syl ⊢ y = A → x | x ∈ y ∈ V → x | x ∈ A ∈ V
7 6 eximi ⊢ ∃ y y = A → ∃ y x | x ∈ y ∈ V → x | x ∈ A ∈ V
8 bj-eximcom ⊢ ∃ y x | x ∈ y ∈ V → x | x ∈ A ∈ V → ∀ y x | x ∈ y ∈ V → ∃ y x | x ∈ A ∈ V
9 8 com12 ⊢ ∀ y x | x ∈ y ∈ V → ∃ y x | x ∈ y ∈ V → x | x ∈ A ∈ V → ∃ y x | x ∈ A ∈ V
10 ax-rep ⊢ ∀ u ∃ z ∀ t ∀ z u = t → t = z → ∃ z ∀ t t ∈ z ↔ ∃ u u ∈ y ∧ ∀ z u = t
11 19.3v ⊢ ∀ z u = t ↔ u = t
12 11 sbbii ⊢ z t ∀ z u = t ↔ z t u = t
13 sbsbc ⊢ z t u = t ↔ [˙z / t]˙ u = t
14 sbceq2g ⊢ z ∈ V → [˙z / t]˙ u = t ↔ u = ⦋ z / t⦌ t
15 14 elv ⊢ [˙z / t]˙ u = t ↔ u = ⦋ z / t⦌ t
16 13 15 bitri ⊢ z t u = t ↔ u = ⦋ z / t⦌ t
17 bj-csbsn ⊢ ⦋ z / t⦌ t = z
18 17 eqeq2i ⊢ u = ⦋ z / t⦌ t ↔ u = z
19 16 18 bitri ⊢ z t u = t ↔ u = z
20 eqtr2 ⊢ u = t ∧ u = z → t = z
21 vex ⊢ t ∈ V
22 21 sneqr ⊢ t = z → t = z
23 20 22 syl ⊢ u = t ∧ u = z → t = z
24 19 23 sylan2b ⊢ u = t ∧ z t u = t → t = z
25 11 12 24 syl2anb ⊢ ∀ z u = t ∧ z t ∀ z u = t → t = z
26 25 gen2 ⊢ ∀ t ∀ z ∀ z u = t ∧ z t ∀ z u = t → t = z
27 nfa1 ⊢ Ⅎ z ∀ z u = t
28 27 mo ⊢ ∃ z ∀ t ∀ z u = t → t = z ↔ ∀ t ∀ z ∀ z u = t ∧ z t ∀ z u = t → t = z
29 26 28 mpbir ⊢ ∃ z ∀ t ∀ z u = t → t = z
30 10 29 mpg ⊢ ∃ z ∀ t t ∈ z ↔ ∃ u u ∈ y ∧ ∀ z u = t
31 bj-sbel1 ⊢ t x x ∈ y ↔ ⦋ t / x⦌ x ∈ y
32 bj-csbsn ⊢ ⦋ t / x⦌ x = t
33 32 eleq1i ⊢ ⦋ t / x⦌ x ∈ y ↔ t ∈ y
34 31 33 bitri ⊢ t x x ∈ y ↔ t ∈ y
35 df-clab ⊢ t ∈ x | x ∈ y ↔ t x x ∈ y
36 11 anbi2i ⊢ u ∈ y ∧ ∀ z u = t ↔ u ∈ y ∧ u = t
37 eleq1a ⊢ u ∈ y → t = u → t ∈ y
38 37 com12 ⊢ t = u → u ∈ y → t ∈ y
39 38 eqcoms ⊢ u = t → u ∈ y → t ∈ y
40 39 imdistanri ⊢ u ∈ y ∧ u = t → t ∈ y ∧ u = t
41 eleq1a ⊢ t ∈ y → u = t → u ∈ y
42 41 impac ⊢ t ∈ y ∧ u = t → u ∈ y ∧ u = t
43 40 42 impbii ⊢ u ∈ y ∧ u = t ↔ t ∈ y ∧ u = t
44 36 43 bitri ⊢ u ∈ y ∧ ∀ z u = t ↔ t ∈ y ∧ u = t
45 44 exbii ⊢ ∃ u u ∈ y ∧ ∀ z u = t ↔ ∃ u t ∈ y ∧ u = t
46 vsnex ⊢ t ∈ V
47 46 isseti ⊢ ∃ u u = t
48 19.42v ⊢ ∃ u t ∈ y ∧ u = t ↔ t ∈ y ∧ ∃ u u = t
49 47 48 mpbiran2 ⊢ ∃ u t ∈ y ∧ u = t ↔ t ∈ y
50 45 49 bitri ⊢ ∃ u u ∈ y ∧ ∀ z u = t ↔ t ∈ y
51 34 35 50 3bitr4ri ⊢ ∃ u u ∈ y ∧ ∀ z u = t ↔ t ∈ x | x ∈ y
52 51 bibi2i ⊢ t ∈ z ↔ ∃ u u ∈ y ∧ ∀ z u = t ↔ t ∈ z ↔ t ∈ x | x ∈ y
53 52 albii ⊢ ∀ t t ∈ z ↔ ∃ u u ∈ y ∧ ∀ z u = t ↔ ∀ t t ∈ z ↔ t ∈ x | x ∈ y
54 53 exbii ⊢ ∃ z ∀ t t ∈ z ↔ ∃ u u ∈ y ∧ ∀ z u = t ↔ ∃ z ∀ t t ∈ z ↔ t ∈ x | x ∈ y
55 30 54 mpbi ⊢ ∃ z ∀ t t ∈ z ↔ t ∈ x | x ∈ y
56 dfcleq ⊢ z = x | x ∈ y ↔ ∀ t t ∈ z ↔ t ∈ x | x ∈ y
57 56 exbii ⊢ ∃ z z = x | x ∈ y ↔ ∃ z ∀ t t ∈ z ↔ t ∈ x | x ∈ y
58 55 57 mpbir ⊢ ∃ z z = x | x ∈ y
59 58 issetri ⊢ x | x ∈ y ∈ V
60 9 59 mpg ⊢ ∃ y x | x ∈ y ∈ V → x | x ∈ A ∈ V → ∃ y x | x ∈ A ∈ V
61 ax5e ⊢ ∃ y x | x ∈ A ∈ V → x | x ∈ A ∈ V
62 1 7 60 61 4syl ⊢ A ∈ V → x | x ∈ A ∈ V