Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  ax-sscoll GIF version

Axiom ax-sscoll 11351
Description: Axiom scheme of subset collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. (Contributed by BJ, 5-Oct-2019.)
Assertion
Ref Expression
ax-sscoll 𝑎𝑏𝑐𝑧(∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐𝑦(𝑦𝑑 ↔ ∃𝑥𝑎 𝜑))
Distinct variable groups:   𝑎,𝑏,𝑐,𝑑,𝑥,𝑦,𝑧   𝜑,𝑎,𝑏,𝑐,𝑑
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Detailed syntax breakdown of Axiom ax-sscoll
StepHypRef Expression
1 wph . . . . . . . 8 wff 𝜑
2 vy . . . . . . . 8 setvar 𝑦
3 vb . . . . . . . . 9 setvar 𝑏
43cv 1286 . . . . . . . 8 class 𝑏
51, 2, 4wrex 2356 . . . . . . 7 wff 𝑦𝑏 𝜑
6 vx . . . . . . 7 setvar 𝑥
7 va . . . . . . . 8 setvar 𝑎
87cv 1286 . . . . . . 7 class 𝑎
95, 6, 8wral 2355 . . . . . 6 wff 𝑥𝑎𝑦𝑏 𝜑
10 vd . . . . . . . . . 10 setvar 𝑑
112, 10wel 1437 . . . . . . . . 9 wff 𝑦𝑑
121, 6, 8wrex 2356 . . . . . . . . 9 wff 𝑥𝑎 𝜑
1311, 12wb 103 . . . . . . . 8 wff (𝑦𝑑 ↔ ∃𝑥𝑎 𝜑)
1413, 2wal 1285 . . . . . . 7 wff 𝑦(𝑦𝑑 ↔ ∃𝑥𝑎 𝜑)
15 vc . . . . . . . 8 setvar 𝑐
1615cv 1286 . . . . . . 7 class 𝑐
1714, 10, 16wrex 2356 . . . . . 6 wff 𝑑𝑐𝑦(𝑦𝑑 ↔ ∃𝑥𝑎 𝜑)
189, 17wi 4 . . . . 5 wff (∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐𝑦(𝑦𝑑 ↔ ∃𝑥𝑎 𝜑))
19 vz . . . . 5 setvar 𝑧
2018, 19wal 1285 . . . 4 wff 𝑧(∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐𝑦(𝑦𝑑 ↔ ∃𝑥𝑎 𝜑))
2120, 15wex 1424 . . 3 wff 𝑐𝑧(∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐𝑦(𝑦𝑑 ↔ ∃𝑥𝑎 𝜑))
2221, 3wal 1285 . 2 wff 𝑏𝑐𝑧(∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐𝑦(𝑦𝑑 ↔ ∃𝑥𝑎 𝜑))
2322, 7wal 1285 1 wff 𝑎𝑏𝑐𝑧(∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐𝑦(𝑦𝑑 ↔ ∃𝑥𝑎 𝜑))
Colors of variables: wff set class
This axiom is referenced by:  sscoll2  11352
  Copyright terms: Public domain W3C validator