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

Axiom ax-strcoll 13977
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  ph represents a multivalued function on  a, or equivalently a collection of nonempty classes indexed by  a, and the axiom asserts the existence of a set  b which "collects" at least one element in the image of each  x  e.  a 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.)
Assertion
Ref Expression
ax-strcoll  |-  A. a
( A. x  e.  a  E. y ph  ->  E. b ( A. x  e.  a  E. y  e.  b  ph  /\ 
A. y  e.  b  E. x  e.  a 
ph ) )
Distinct variable groups:    a, b, x, y    ph, a, b
Allowed substitution hints:    ph( x, y)

Detailed syntax breakdown of Axiom ax-strcoll
StepHypRef Expression
1 wph . . . . 5  wff  ph
2 vy . . . . 5  setvar  y
31, 2wex 1485 . . . 4  wff  E. y ph
4 vx . . . 4  setvar  x
5 va . . . . 5  setvar  a
65cv 1347 . . . 4  class  a
73, 4, 6wral 2448 . . 3  wff  A. x  e.  a  E. y ph
8 vb . . . . . . . 8  setvar  b
98cv 1347 . . . . . . 7  class  b
101, 2, 9wrex 2449 . . . . . 6  wff  E. y  e.  b  ph
1110, 4, 6wral 2448 . . . . 5  wff  A. x  e.  a  E. y  e.  b  ph
121, 4, 6wrex 2449 . . . . . 6  wff  E. x  e.  a  ph
1312, 2, 9wral 2448 . . . . 5  wff  A. y  e.  b  E. x  e.  a  ph
1411, 13wa 103 . . . 4  wff  ( A. x  e.  a  E. y  e.  b  ph  /\ 
A. y  e.  b  E. x  e.  a 
ph )
1514, 8wex 1485 . . 3  wff  E. b
( A. x  e.  a  E. y  e.  b  ph  /\  A. y  e.  b  E. x  e.  a  ph )
167, 15wi 4 . 2  wff  ( A. x  e.  a  E. y ph  ->  E. b
( A. x  e.  a  E. y  e.  b  ph  /\  A. y  e.  b  E. x  e.  a  ph ) )
1716, 5wal 1346 1  wff  A. a
( A. x  e.  a  E. y ph  ->  E. b ( A. x  e.  a  E. y  e.  b  ph  /\ 
A. y  e.  b  E. x  e.  a 
ph ) )
Colors of variables: wff set class
This axiom is referenced by:  strcoll2  13978
  Copyright terms: Public domain W3C validator