Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  exss GIF version

Theorem exss 3963
 Description: Restricted existence in a class (even if proper) implies restricted existence in a subset. (Contributed by NM, 23-Aug-2003.)
Assertion
Ref Expression
exss (∃𝑥𝐴 𝜑 → ∃𝑦(𝑦𝐴 ∧ ∃𝑥𝑦 𝜑))
Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem exss
Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rabn0m 3245 . . 3 (∃𝑧 𝑧 ∈ {𝑥𝐴𝜑} ↔ ∃𝑥𝐴 𝜑)
2 df-rab 2315 . . . . 5 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
32eleq2i 2104 . . . 4 (𝑧 ∈ {𝑥𝐴𝜑} ↔ 𝑧 ∈ {𝑥 ∣ (𝑥𝐴𝜑)})
43exbii 1496 . . 3 (∃𝑧 𝑧 ∈ {𝑥𝐴𝜑} ↔ ∃𝑧 𝑧 ∈ {𝑥 ∣ (𝑥𝐴𝜑)})
51, 4bitr3i 175 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑧 𝑧 ∈ {𝑥 ∣ (𝑥𝐴𝜑)})
6 vex 2560 . . . . . 6 𝑧 ∈ V
76snss 3494 . . . . 5 (𝑧 ∈ {𝑥 ∣ (𝑥𝐴𝜑)} ↔ {𝑧} ⊆ {𝑥 ∣ (𝑥𝐴𝜑)})
8 ssab2 3024 . . . . . 6 {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ 𝐴
9 sstr2 2952 . . . . . 6 ({𝑧} ⊆ {𝑥 ∣ (𝑥𝐴𝜑)} → ({𝑥 ∣ (𝑥𝐴𝜑)} ⊆ 𝐴 → {𝑧} ⊆ 𝐴))
108, 9mpi 15 . . . . 5 ({𝑧} ⊆ {𝑥 ∣ (𝑥𝐴𝜑)} → {𝑧} ⊆ 𝐴)
117, 10sylbi 114 . . . 4 (𝑧 ∈ {𝑥 ∣ (𝑥𝐴𝜑)} → {𝑧} ⊆ 𝐴)
12 simpr 103 . . . . . . . 8 (([𝑧 / 𝑥]𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑) → [𝑧 / 𝑥]𝜑)
13 equsb1 1668 . . . . . . . . 9 [𝑧 / 𝑥]𝑥 = 𝑧
14 velsn 3392 . . . . . . . . . 10 (𝑥 ∈ {𝑧} ↔ 𝑥 = 𝑧)
1514sbbii 1648 . . . . . . . . 9 ([𝑧 / 𝑥]𝑥 ∈ {𝑧} ↔ [𝑧 / 𝑥]𝑥 = 𝑧)
1613, 15mpbir 134 . . . . . . . 8 [𝑧 / 𝑥]𝑥 ∈ {𝑧}
1712, 16jctil 295 . . . . . . 7 (([𝑧 / 𝑥]𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑) → ([𝑧 / 𝑥]𝑥 ∈ {𝑧} ∧ [𝑧 / 𝑥]𝜑))
18 df-clab 2027 . . . . . . . 8 (𝑧 ∈ {𝑥 ∣ (𝑥𝐴𝜑)} ↔ [𝑧 / 𝑥](𝑥𝐴𝜑))
19 sban 1829 . . . . . . . 8 ([𝑧 / 𝑥](𝑥𝐴𝜑) ↔ ([𝑧 / 𝑥]𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑))
2018, 19bitri 173 . . . . . . 7 (𝑧 ∈ {𝑥 ∣ (𝑥𝐴𝜑)} ↔ ([𝑧 / 𝑥]𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑))
21 df-rab 2315 . . . . . . . . 9 {𝑥 ∈ {𝑧} ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ {𝑧} ∧ 𝜑)}
2221eleq2i 2104 . . . . . . . 8 (𝑧 ∈ {𝑥 ∈ {𝑧} ∣ 𝜑} ↔ 𝑧 ∈ {𝑥 ∣ (𝑥 ∈ {𝑧} ∧ 𝜑)})
23 df-clab 2027 . . . . . . . . 9 (𝑧 ∈ {𝑥 ∣ (𝑥 ∈ {𝑧} ∧ 𝜑)} ↔ [𝑧 / 𝑥](𝑥 ∈ {𝑧} ∧ 𝜑))
24 sban 1829 . . . . . . . . 9 ([𝑧 / 𝑥](𝑥 ∈ {𝑧} ∧ 𝜑) ↔ ([𝑧 / 𝑥]𝑥 ∈ {𝑧} ∧ [𝑧 / 𝑥]𝜑))
2523, 24bitri 173 . . . . . . . 8 (𝑧 ∈ {𝑥 ∣ (𝑥 ∈ {𝑧} ∧ 𝜑)} ↔ ([𝑧 / 𝑥]𝑥 ∈ {𝑧} ∧ [𝑧 / 𝑥]𝜑))
2622, 25bitri 173 . . . . . . 7 (𝑧 ∈ {𝑥 ∈ {𝑧} ∣ 𝜑} ↔ ([𝑧 / 𝑥]𝑥 ∈ {𝑧} ∧ [𝑧 / 𝑥]𝜑))
2717, 20, 263imtr4i 190 . . . . . 6 (𝑧 ∈ {𝑥 ∣ (𝑥𝐴𝜑)} → 𝑧 ∈ {𝑥 ∈ {𝑧} ∣ 𝜑})
28 elex2 2570 . . . . . 6 (𝑧 ∈ {𝑥 ∈ {𝑧} ∣ 𝜑} → ∃𝑤 𝑤 ∈ {𝑥 ∈ {𝑧} ∣ 𝜑})
2927, 28syl 14 . . . . 5 (𝑧 ∈ {𝑥 ∣ (𝑥𝐴𝜑)} → ∃𝑤 𝑤 ∈ {𝑥 ∈ {𝑧} ∣ 𝜑})
30 rabn0m 3245 . . . . 5 (∃𝑤 𝑤 ∈ {𝑥 ∈ {𝑧} ∣ 𝜑} ↔ ∃𝑥 ∈ {𝑧}𝜑)
3129, 30sylib 127 . . . 4 (𝑧 ∈ {𝑥 ∣ (𝑥𝐴𝜑)} → ∃𝑥 ∈ {𝑧}𝜑)
32 snexgOLD 3935 . . . . . 6 (𝑧 ∈ V → {𝑧} ∈ V)
336, 32ax-mp 7 . . . . 5 {𝑧} ∈ V
34 sseq1 2966 . . . . . 6 (𝑦 = {𝑧} → (𝑦𝐴 ↔ {𝑧} ⊆ 𝐴))
35 rexeq 2506 . . . . . 6 (𝑦 = {𝑧} → (∃𝑥𝑦 𝜑 ↔ ∃𝑥 ∈ {𝑧}𝜑))
3634, 35anbi12d 442 . . . . 5 (𝑦 = {𝑧} → ((𝑦𝐴 ∧ ∃𝑥𝑦 𝜑) ↔ ({𝑧} ⊆ 𝐴 ∧ ∃𝑥 ∈ {𝑧}𝜑)))
3733, 36spcev 2647 . . . 4 (({𝑧} ⊆ 𝐴 ∧ ∃𝑥 ∈ {𝑧}𝜑) → ∃𝑦(𝑦𝐴 ∧ ∃𝑥𝑦 𝜑))
3811, 31, 37syl2anc 391 . . 3 (𝑧 ∈ {𝑥 ∣ (𝑥𝐴𝜑)} → ∃𝑦(𝑦𝐴 ∧ ∃𝑥𝑦 𝜑))
3938exlimiv 1489 . 2 (∃𝑧 𝑧 ∈ {𝑥 ∣ (𝑥𝐴𝜑)} → ∃𝑦(𝑦𝐴 ∧ ∃𝑥𝑦 𝜑))
405, 39sylbi 114 1 (∃𝑥𝐴 𝜑 → ∃𝑦(𝑦𝐴 ∧ ∃𝑥𝑦 𝜑))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   = wceq 1243  ∃wex 1381   ∈ wcel 1393  [wsb 1645  {cab 2026  ∃wrex 2307  {crab 2310  Vcvv 2557   ⊆ wss 2917  {csn 3375 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927 This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-rab 2315  df-v 2559  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator