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