Theorem bj-snsetex 36148

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

Assertion

Ref	Expression
bj-snsetex	⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem bj-snsetex

Dummy variables 𝑦 𝑧 𝑡 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elisset 2814	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ∃𝑦 𝑦 = 𝐴)
2		eleq2 2821	. . . . . . 7 ⊢ (𝑦 = 𝐴 → ({𝑥} ∈ 𝑦 ↔ {𝑥} ∈ 𝐴))
3	2	abbidv 2800	. . . . . 6 ⊢ (𝑦 = 𝐴 → {𝑥 ∣ {𝑥} ∈ 𝑦} = {𝑥 ∣ {𝑥} ∈ 𝐴})
4		eleq1 2820	. . . . . . 7 ⊢ ({𝑥 ∣ {𝑥} ∈ 𝑦} = {𝑥 ∣ {𝑥} ∈ 𝐴} → ({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V ↔ {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V))
5	4	biimpd 228	. . . . . 6 ⊢ ({𝑥 ∣ {𝑥} ∈ 𝑦} = {𝑥 ∣ {𝑥} ∈ 𝐴} → ({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V))
6	3, 5	syl 17	. . . . 5 ⊢ (𝑦 = 𝐴 → ({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V))
7	6	eximi 1836	. . . 4 ⊢ (∃𝑦 𝑦 = 𝐴 → ∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V))
8	1, 7	syl 17	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V))
9		bj-eximcom 35824	. . . . 5 ⊢ (∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) → (∀𝑦{𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V))
10	9	com12 32	. . . 4 ⊢ (∀𝑦{𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → (∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V))
11		ax-rep 5285	. . . . . . . 8 ⊢ (∀𝑢∃𝑧∀𝑡(∀𝑧 𝑢 = {𝑡} → 𝑡 = 𝑧) → ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})))
12		19.3v 1984	. . . . . . . . . . 11 ⊢ (∀𝑧 𝑢 = {𝑡} ↔ 𝑢 = {𝑡})
13	12	sbbii 2078	. . . . . . . . . . 11 ⊢ ([𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡} ↔ [𝑧 / 𝑡]𝑢 = {𝑡})
14		sbsbc 3781	. . . . . . . . . . . . . 14 ⊢ ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ [𝑧 / 𝑡]𝑢 = {𝑡})
15		sbceq2g 4416	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = ⦋𝑧 / 𝑡⦌{𝑡}))
16	15	elv 3479	. . . . . . . . . . . . . 14 ⊢ ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = ⦋𝑧 / 𝑡⦌{𝑡})
17	14, 16	bitri 275	. . . . . . . . . . . . 13 ⊢ ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = ⦋𝑧 / 𝑡⦌{𝑡})
18		bj-csbsn 36088	. . . . . . . . . . . . . 14 ⊢ ⦋𝑧 / 𝑡⦌{𝑡} = {𝑧}
19	18	eqeq2i 2744	. . . . . . . . . . . . 13 ⊢ (𝑢 = ⦋𝑧 / 𝑡⦌{𝑡} ↔ 𝑢 = {𝑧})
20	17, 19	bitri 275	. . . . . . . . . . . 12 ⊢ ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = {𝑧})
21		eqtr2 2755	. . . . . . . . . . . . 13 ⊢ ((𝑢 = {𝑡} ∧ 𝑢 = {𝑧}) → {𝑡} = {𝑧})
22		vex 3477	. . . . . . . . . . . . . 14 ⊢ 𝑡 ∈ V
23	22	sneqr 4841	. . . . . . . . . . . . 13 ⊢ ({𝑡} = {𝑧} → 𝑡 = 𝑧)
24	21, 23	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑢 = {𝑡} ∧ 𝑢 = {𝑧}) → 𝑡 = 𝑧)
25	20, 24	sylan2b 593	. . . . . . . . . . 11 ⊢ ((𝑢 = {𝑡} ∧ [𝑧 / 𝑡]𝑢 = {𝑡}) → 𝑡 = 𝑧)
26	12, 13, 25	syl2anb 597	. . . . . . . . . 10 ⊢ ((∀𝑧 𝑢 = {𝑡} ∧ [𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡}) → 𝑡 = 𝑧)
27	26	gen2 1797	. . . . . . . . 9 ⊢ ∀𝑡∀𝑧((∀𝑧 𝑢 = {𝑡} ∧ [𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡}) → 𝑡 = 𝑧)
28		nfa1 2147	. . . . . . . . . 10 ⊢ Ⅎ𝑧∀𝑧 𝑢 = {𝑡}
29	28	mo 2558	. . . . . . . . 9 ⊢ (∃𝑧∀𝑡(∀𝑧 𝑢 = {𝑡} → 𝑡 = 𝑧) ↔ ∀𝑡∀𝑧((∀𝑧 𝑢 = {𝑡} ∧ [𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡}) → 𝑡 = 𝑧))
30	27, 29	mpbir 230	. . . . . . . 8 ⊢ ∃𝑧∀𝑡(∀𝑧 𝑢 = {𝑡} → 𝑡 = 𝑧)
31	11, 30	mpg 1798	. . . . . . 7 ⊢ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}))
32		bj-sbel1 36089	. . . . . . . . . . . 12 ⊢ ([𝑡 / 𝑥]{𝑥} ∈ 𝑦 ↔ ⦋𝑡 / 𝑥⦌{𝑥} ∈ 𝑦)
33		bj-csbsn 36088	. . . . . . . . . . . . 13 ⊢ ⦋𝑡 / 𝑥⦌{𝑥} = {𝑡}
34	33	eleq1i 2823	. . . . . . . . . . . 12 ⊢ (⦋𝑡 / 𝑥⦌{𝑥} ∈ 𝑦 ↔ {𝑡} ∈ 𝑦)
35	32, 34	bitri 275	. . . . . . . . . . 11 ⊢ ([𝑡 / 𝑥]{𝑥} ∈ 𝑦 ↔ {𝑡} ∈ 𝑦)
36		df-clab 2709	. . . . . . . . . . 11 ⊢ (𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦} ↔ [𝑡 / 𝑥]{𝑥} ∈ 𝑦)
37	12	anbi2i 622	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ (𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡}))
38		eleq1a 2827	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ 𝑦 → ({𝑡} = 𝑢 → {𝑡} ∈ 𝑦))
39	38	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑡} = 𝑢 → (𝑢 ∈ 𝑦 → {𝑡} ∈ 𝑦))
40	39	eqcoms 2739	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = {𝑡} → (𝑢 ∈ 𝑦 → {𝑡} ∈ 𝑦))
41	40	imdistanri 569	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡}) → ({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}))
42		eleq1a 2827	. . . . . . . . . . . . . . . 16 ⊢ ({𝑡} ∈ 𝑦 → (𝑢 = {𝑡} → 𝑢 ∈ 𝑦))
43	42	impac 552	. . . . . . . . . . . . . . 15 ⊢ (({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}) → (𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡}))
44	41, 43	impbii 208	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ 𝑦 ∧ 𝑢 = {𝑡}) ↔ ({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}))
45	37, 44	bitri 275	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ ({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}))
46	45	exbii 1849	. . . . . . . . . . . 12 ⊢ (∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ ∃𝑢({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}))
47		vsnex 5429	. . . . . . . . . . . . . 14 ⊢ {𝑡} ∈ V
48	47	isseti 3489	. . . . . . . . . . . . 13 ⊢ ∃𝑢 𝑢 = {𝑡}
49		19.42v 1956	. . . . . . . . . . . . 13 ⊢ (∃𝑢({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}) ↔ ({𝑡} ∈ 𝑦 ∧ ∃𝑢 𝑢 = {𝑡}))
50	48, 49	mpbiran2 707	. . . . . . . . . . . 12 ⊢ (∃𝑢({𝑡} ∈ 𝑦 ∧ 𝑢 = {𝑡}) ↔ {𝑡} ∈ 𝑦)
51	46, 50	bitri 275	. . . . . . . . . . 11 ⊢ (∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ {𝑡} ∈ 𝑦)
52	35, 36, 51	3bitr4ri 304	. . . . . . . . . 10 ⊢ (∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})
53	52	bibi2i 337	. . . . . . . . 9 ⊢ ((𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) ↔ (𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}))
54	53	albii 1820	. . . . . . . 8 ⊢ (∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) ↔ ∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}))
55	54	exbii 1849	. . . . . . 7 ⊢ (∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ ∃𝑢(𝑢 ∈ 𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}))
56	31, 55	mpbi 229	. . . . . 6 ⊢ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})
57		dfcleq 2724	. . . . . . 7 ⊢ (𝑧 = {𝑥 ∣ {𝑥} ∈ 𝑦} ↔ ∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}))
58	57	exbii 1849	. . . . . 6 ⊢ (∃𝑧 𝑧 = {𝑥 ∣ {𝑥} ∈ 𝑦} ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}))
59	56, 58	mpbir 230	. . . . 5 ⊢ ∃𝑧 𝑧 = {𝑥 ∣ {𝑥} ∈ 𝑦}
60	59	issetri 3490	. . . 4 ⊢ {𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V
61	10, 60	mpg 1798	. . 3 ⊢ (∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)
62	8, 61	syl 17	. 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)
63		ax5e 1914	. 2 ⊢ (∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)
64	62, 63	syl 17	1 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1780  [wsb 2066   ∈ wcel 2105  {cab 2708  Vcvv 3473  [wsbc 3777  ⦋csb 3893  {csn 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-nul 4323  df-sn 4629  df-pr 4631

This theorem is referenced by:  bj-clexab  36149  bj-snglex  36158