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

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