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

Axiom ax-strcoll 15212
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 4133. (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 1503 . . . 4 wff 𝑦𝜑
4 vx . . . 4 setvar 𝑥
5 va . . . . 5 setvar 𝑎
65cv 1363 . . . 4 class 𝑎
73, 4, 6wral 2468 . . 3 wff 𝑥𝑎𝑦𝜑
8 vb . . . . . . . 8 setvar 𝑏
98cv 1363 . . . . . . 7 class 𝑏
101, 2, 9wrex 2469 . . . . . 6 wff 𝑦𝑏 𝜑
1110, 4, 6wral 2468 . . . . 5 wff 𝑥𝑎𝑦𝑏 𝜑
121, 4, 6wrex 2469 . . . . . 6 wff 𝑥𝑎 𝜑
1312, 2, 9wral 2468 . . . . 5 wff 𝑦𝑏𝑥𝑎 𝜑
1411, 13wa 104 . . . 4 wff (∀𝑥𝑎𝑦𝑏 𝜑 ∧ ∀𝑦𝑏𝑥𝑎 𝜑)
1514, 8wex 1503 . . 3 wff 𝑏(∀𝑥𝑎𝑦𝑏 𝜑 ∧ ∀𝑦𝑏𝑥𝑎 𝜑)
167, 15wi 4 . 2 wff (∀𝑥𝑎𝑦𝜑 → ∃𝑏(∀𝑥𝑎𝑦𝑏 𝜑 ∧ ∀𝑦𝑏𝑥𝑎 𝜑))
1716, 5wal 1362 1 wff 𝑎(∀𝑥𝑎𝑦𝜑 → ∃𝑏(∀𝑥𝑎𝑦𝑏 𝜑 ∧ ∀𝑦𝑏𝑥𝑎 𝜑))
Colors of variables: wff set class
This axiom is referenced by:  strcoll2  15213
  Copyright terms: Public domain W3C validator