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

Axiom ax-strcoll 13107
Description: Axiom scheme of strong 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-strcoll 𝑎(∀𝑥𝑎𝑦𝜑 → ∃𝑏𝑦(𝑦𝑏 ↔ ∃𝑥𝑎 𝜑))
Distinct variable groups:   𝑎,𝑏,𝑥,𝑦   𝜑,𝑎,𝑏
Allowed substitution hints:   𝜑(𝑥,𝑦)

Detailed syntax breakdown of Axiom ax-strcoll
StepHypRef Expression
1 wph . . . . 5 wff 𝜑
2 vy . . . . 5 setvar 𝑦
31, 2wex 1453 . . . 4 wff 𝑦𝜑
4 vx . . . 4 setvar 𝑥
5 va . . . . 5 setvar 𝑎
65cv 1315 . . . 4 class 𝑎
73, 4, 6wral 2393 . . 3 wff 𝑥𝑎𝑦𝜑
8 vb . . . . . . 7 setvar 𝑏
92, 8wel 1466 . . . . . 6 wff 𝑦𝑏
101, 4, 6wrex 2394 . . . . . 6 wff 𝑥𝑎 𝜑
119, 10wb 104 . . . . 5 wff (𝑦𝑏 ↔ ∃𝑥𝑎 𝜑)
1211, 2wal 1314 . . . 4 wff 𝑦(𝑦𝑏 ↔ ∃𝑥𝑎 𝜑)
1312, 8wex 1453 . . 3 wff 𝑏𝑦(𝑦𝑏 ↔ ∃𝑥𝑎 𝜑)
147, 13wi 4 . 2 wff (∀𝑥𝑎𝑦𝜑 → ∃𝑏𝑦(𝑦𝑏 ↔ ∃𝑥𝑎 𝜑))
1514, 5wal 1314 1 wff 𝑎(∀𝑥𝑎𝑦𝜑 → ∃𝑏𝑦(𝑦𝑏 ↔ ∃𝑥𝑎 𝜑))
Colors of variables: wff set class
This axiom is referenced by:  strcoll2  13108
  Copyright terms: Public domain W3C validator