Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > Mathboxes > ax-strcoll | Unicode version |
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 4102. (Contributed by BJ, 5-Oct-2019.) |
Ref | Expression |
---|---|
ax-strcoll |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . . . 5 | |
2 | vy | . . . . 5 | |
3 | 1, 2 | wex 1485 | . . . 4 |
4 | vx | . . . 4 | |
5 | va | . . . . 5 | |
6 | 5 | cv 1347 | . . . 4 |
7 | 3, 4, 6 | wral 2448 | . . 3 |
8 | vb | . . . . . . . 8 | |
9 | 8 | cv 1347 | . . . . . . 7 |
10 | 1, 2, 9 | wrex 2449 | . . . . . 6 |
11 | 10, 4, 6 | wral 2448 | . . . . 5 |
12 | 1, 4, 6 | wrex 2449 | . . . . . 6 |
13 | 12, 2, 9 | wral 2448 | . . . . 5 |
14 | 11, 13 | wa 103 | . . . 4 |
15 | 14, 8 | wex 1485 | . . 3 |
16 | 7, 15 | wi 4 | . 2 |
17 | 16, 5 | wal 1346 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: strcoll2 13978 |
Copyright terms: Public domain | W3C validator |