Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-snsetex Structured version   Visualization version   GIF version

Theorem bj-snsetex 36683
Description: The class of sets "whose singletons" belong to a set is a set. Nice application of ax-rep 5282. (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.
StepHypRef Expression
1 elisset 2808 . 2 (𝐴𝑉 → ∃𝑦 𝑦 = 𝐴)
2 eleq2 2815 . . . . 5 (𝑦 = 𝐴 → ({𝑥} ∈ 𝑦 ↔ {𝑥} ∈ 𝐴))
32abbidv 2795 . . . 4 (𝑦 = 𝐴 → {𝑥 ∣ {𝑥} ∈ 𝑦} = {𝑥 ∣ {𝑥} ∈ 𝐴})
4 eleq1 2814 . . . . 5 ({𝑥 ∣ {𝑥} ∈ 𝑦} = {𝑥 ∣ {𝑥} ∈ 𝐴} → ({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V ↔ {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V))
54biimpd 228 . . . 4 ({𝑥 ∣ {𝑥} ∈ 𝑦} = {𝑥 ∣ {𝑥} ∈ 𝐴} → ({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V))
63, 5syl 17 . . 3 (𝑦 = 𝐴 → ({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V))
76eximi 1830 . 2 (∃𝑦 𝑦 = 𝐴 → ∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V))
8 bj-eximcom 36360 . . . 4 (∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) → (∀𝑦{𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V))
98com12 32 . . 3 (∀𝑦{𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → (∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V))
10 ax-rep 5282 . . . . . . 7 (∀𝑢𝑧𝑡(∀𝑧 𝑢 = {𝑡} → 𝑡 = 𝑧) → ∃𝑧𝑡(𝑡𝑧 ↔ ∃𝑢(𝑢𝑦 ∧ ∀𝑧 𝑢 = {𝑡})))
11 19.3v 1978 . . . . . . . . . 10 (∀𝑧 𝑢 = {𝑡} ↔ 𝑢 = {𝑡})
1211sbbii 2072 . . . . . . . . . 10 ([𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡} ↔ [𝑧 / 𝑡]𝑢 = {𝑡})
13 sbsbc 3779 . . . . . . . . . . . . 13 ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ [𝑧 / 𝑡]𝑢 = {𝑡})
14 sbceq2g 4413 . . . . . . . . . . . . . 14 (𝑧 ∈ V → ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = 𝑧 / 𝑡{𝑡}))
1514elv 3468 . . . . . . . . . . . . 13 ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = 𝑧 / 𝑡{𝑡})
1613, 15bitri 274 . . . . . . . . . . . 12 ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = 𝑧 / 𝑡{𝑡})
17 bj-csbsn 36623 . . . . . . . . . . . . 13 𝑧 / 𝑡{𝑡} = {𝑧}
1817eqeq2i 2739 . . . . . . . . . . . 12 (𝑢 = 𝑧 / 𝑡{𝑡} ↔ 𝑢 = {𝑧})
1916, 18bitri 274 . . . . . . . . . . 11 ([𝑧 / 𝑡]𝑢 = {𝑡} ↔ 𝑢 = {𝑧})
20 eqtr2 2750 . . . . . . . . . . . 12 ((𝑢 = {𝑡} ∧ 𝑢 = {𝑧}) → {𝑡} = {𝑧})
21 vex 3466 . . . . . . . . . . . . 13 𝑡 ∈ V
2221sneqr 4839 . . . . . . . . . . . 12 ({𝑡} = {𝑧} → 𝑡 = 𝑧)
2320, 22syl 17 . . . . . . . . . . 11 ((𝑢 = {𝑡} ∧ 𝑢 = {𝑧}) → 𝑡 = 𝑧)
2419, 23sylan2b 592 . . . . . . . . . 10 ((𝑢 = {𝑡} ∧ [𝑧 / 𝑡]𝑢 = {𝑡}) → 𝑡 = 𝑧)
2511, 12, 24syl2anb 596 . . . . . . . . 9 ((∀𝑧 𝑢 = {𝑡} ∧ [𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡}) → 𝑡 = 𝑧)
2625gen2 1791 . . . . . . . 8 𝑡𝑧((∀𝑧 𝑢 = {𝑡} ∧ [𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡}) → 𝑡 = 𝑧)
27 nfa1 2141 . . . . . . . . 9 𝑧𝑧 𝑢 = {𝑡}
2827mo 2554 . . . . . . . 8 (∃𝑧𝑡(∀𝑧 𝑢 = {𝑡} → 𝑡 = 𝑧) ↔ ∀𝑡𝑧((∀𝑧 𝑢 = {𝑡} ∧ [𝑧 / 𝑡]∀𝑧 𝑢 = {𝑡}) → 𝑡 = 𝑧))
2926, 28mpbir 230 . . . . . . 7 𝑧𝑡(∀𝑧 𝑢 = {𝑡} → 𝑡 = 𝑧)
3010, 29mpg 1792 . . . . . 6 𝑧𝑡(𝑡𝑧 ↔ ∃𝑢(𝑢𝑦 ∧ ∀𝑧 𝑢 = {𝑡}))
31 bj-sbel1 36624 . . . . . . . . . . 11 ([𝑡 / 𝑥]{𝑥} ∈ 𝑦𝑡 / 𝑥{𝑥} ∈ 𝑦)
32 bj-csbsn 36623 . . . . . . . . . . . 12 𝑡 / 𝑥{𝑥} = {𝑡}
3332eleq1i 2817 . . . . . . . . . . 11 (𝑡 / 𝑥{𝑥} ∈ 𝑦 ↔ {𝑡} ∈ 𝑦)
3431, 33bitri 274 . . . . . . . . . 10 ([𝑡 / 𝑥]{𝑥} ∈ 𝑦 ↔ {𝑡} ∈ 𝑦)
35 df-clab 2704 . . . . . . . . . 10 (𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦} ↔ [𝑡 / 𝑥]{𝑥} ∈ 𝑦)
3611anbi2i 621 . . . . . . . . . . . . 13 ((𝑢𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ (𝑢𝑦𝑢 = {𝑡}))
37 eleq1a 2821 . . . . . . . . . . . . . . . . 17 (𝑢𝑦 → ({𝑡} = 𝑢 → {𝑡} ∈ 𝑦))
3837com12 32 . . . . . . . . . . . . . . . 16 ({𝑡} = 𝑢 → (𝑢𝑦 → {𝑡} ∈ 𝑦))
3938eqcoms 2734 . . . . . . . . . . . . . . 15 (𝑢 = {𝑡} → (𝑢𝑦 → {𝑡} ∈ 𝑦))
4039imdistanri 568 . . . . . . . . . . . . . 14 ((𝑢𝑦𝑢 = {𝑡}) → ({𝑡} ∈ 𝑦𝑢 = {𝑡}))
41 eleq1a 2821 . . . . . . . . . . . . . . 15 ({𝑡} ∈ 𝑦 → (𝑢 = {𝑡} → 𝑢𝑦))
4241impac 551 . . . . . . . . . . . . . 14 (({𝑡} ∈ 𝑦𝑢 = {𝑡}) → (𝑢𝑦𝑢 = {𝑡}))
4340, 42impbii 208 . . . . . . . . . . . . 13 ((𝑢𝑦𝑢 = {𝑡}) ↔ ({𝑡} ∈ 𝑦𝑢 = {𝑡}))
4436, 43bitri 274 . . . . . . . . . . . 12 ((𝑢𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ ({𝑡} ∈ 𝑦𝑢 = {𝑡}))
4544exbii 1843 . . . . . . . . . . 11 (∃𝑢(𝑢𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ ∃𝑢({𝑡} ∈ 𝑦𝑢 = {𝑡}))
46 vsnex 5427 . . . . . . . . . . . . 13 {𝑡} ∈ V
4746isseti 3479 . . . . . . . . . . . 12 𝑢 𝑢 = {𝑡}
48 19.42v 1950 . . . . . . . . . . . 12 (∃𝑢({𝑡} ∈ 𝑦𝑢 = {𝑡}) ↔ ({𝑡} ∈ 𝑦 ∧ ∃𝑢 𝑢 = {𝑡}))
4947, 48mpbiran2 708 . . . . . . . . . . 11 (∃𝑢({𝑡} ∈ 𝑦𝑢 = {𝑡}) ↔ {𝑡} ∈ 𝑦)
5045, 49bitri 274 . . . . . . . . . 10 (∃𝑢(𝑢𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ {𝑡} ∈ 𝑦)
5134, 35, 503bitr4ri 303 . . . . . . . . 9 (∃𝑢(𝑢𝑦 ∧ ∀𝑧 𝑢 = {𝑡}) ↔ 𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})
5251bibi2i 336 . . . . . . . 8 ((𝑡𝑧 ↔ ∃𝑢(𝑢𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) ↔ (𝑡𝑧𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}))
5352albii 1814 . . . . . . 7 (∀𝑡(𝑡𝑧 ↔ ∃𝑢(𝑢𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) ↔ ∀𝑡(𝑡𝑧𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}))
5453exbii 1843 . . . . . 6 (∃𝑧𝑡(𝑡𝑧 ↔ ∃𝑢(𝑢𝑦 ∧ ∀𝑧 𝑢 = {𝑡})) ↔ ∃𝑧𝑡(𝑡𝑧𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}))
5530, 54mpbi 229 . . . . 5 𝑧𝑡(𝑡𝑧𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦})
56 dfcleq 2719 . . . . . 6 (𝑧 = {𝑥 ∣ {𝑥} ∈ 𝑦} ↔ ∀𝑡(𝑡𝑧𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}))
5756exbii 1843 . . . . 5 (∃𝑧 𝑧 = {𝑥 ∣ {𝑥} ∈ 𝑦} ↔ ∃𝑧𝑡(𝑡𝑧𝑡 ∈ {𝑥 ∣ {𝑥} ∈ 𝑦}))
5855, 57mpbir 230 . . . 4 𝑧 𝑧 = {𝑥 ∣ {𝑥} ∈ 𝑦}
5958issetri 3480 . . 3 {𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V
609, 59mpg 1792 . 2 (∃𝑦({𝑥 ∣ {𝑥} ∈ 𝑦} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V) → ∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)
61 ax5e 1908 . 2 (∃𝑦{𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)
621, 7, 60, 614syl 19 1 (𝐴𝑉 → {𝑥 ∣ {𝑥} ∈ 𝐴} ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wal 1532   = wceq 1534  wex 1774  [wsb 2060  wcel 2099  {cab 2703  Vcvv 3462  [wsbc 3775  csb 3891  {csn 4623
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-pr 5425
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-nul 4323  df-sn 4624  df-pr 4626
This theorem is referenced by:  bj-clexab  36684  bj-snglex  36693
  Copyright terms: Public domain W3C validator