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

Axiom ax-strcoll 13628
Description: Axiom scheme of strong collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. The antecedent means that 𝜑 represents a multivalued function on 𝑎, or equivalently a collection of nonempty classes indexed by 𝑎, and the axiom asserts the existence of a set 𝑏 which "collects" at least one element in the image of each 𝑥𝑎 and which is made only of such elements. That second conjunct is what makes it "strong", compared to the axiom scheme of collection ax-coll 4081. (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 1472 . . . 4 wff 𝑦𝜑
4 vx . . . 4 setvar 𝑥
5 va . . . . 5 setvar 𝑎
65cv 1334 . . . 4 class 𝑎
73, 4, 6wral 2435 . . 3 wff 𝑥𝑎𝑦𝜑
8 vb . . . . . . . 8 setvar 𝑏
98cv 1334 . . . . . . 7 class 𝑏
101, 2, 9wrex 2436 . . . . . 6 wff 𝑦𝑏 𝜑
1110, 4, 6wral 2435 . . . . 5 wff 𝑥𝑎𝑦𝑏 𝜑
121, 4, 6wrex 2436 . . . . . 6 wff 𝑥𝑎 𝜑
1312, 2, 9wral 2435 . . . . 5 wff 𝑦𝑏𝑥𝑎 𝜑
1411, 13wa 103 . . . 4 wff (∀𝑥𝑎𝑦𝑏 𝜑 ∧ ∀𝑦𝑏𝑥𝑎 𝜑)
1514, 8wex 1472 . . 3 wff 𝑏(∀𝑥𝑎𝑦𝑏 𝜑 ∧ ∀𝑦𝑏𝑥𝑎 𝜑)
167, 15wi 4 . 2 wff (∀𝑥𝑎𝑦𝜑 → ∃𝑏(∀𝑥𝑎𝑦𝑏 𝜑 ∧ ∀𝑦𝑏𝑥𝑎 𝜑))
1716, 5wal 1333 1 wff 𝑎(∀𝑥𝑎𝑦𝜑 → ∃𝑏(∀𝑥𝑎𝑦𝑏 𝜑 ∧ ∀𝑦𝑏𝑥𝑎 𝜑))
Colors of variables: wff set class
This axiom is referenced by:  strcoll2  13629
  Copyright terms: Public domain W3C validator