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

Axiom ax-strcoll 13107
Description: Axiom scheme of strong collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. (Contributed by BJ, 5-Oct-2019.)
Assertion
Ref Expression
ax-strcoll  |-  A. a
( A. x  e.  a  E. y ph  ->  E. b A. y
( 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 1453 . . . 4  wff  E. y ph
4 vx . . . 4  setvar  x
5 va . . . . 5  setvar  a
65cv 1315 . . . 4  class  a
73, 4, 6wral 2393 . . 3  wff  A. x  e.  a  E. y ph
8 vb . . . . . . 7  setvar  b
92, 8wel 1466 . . . . . 6  wff  y  e.  b
101, 4, 6wrex 2394 . . . . . 6  wff  E. x  e.  a  ph
119, 10wb 104 . . . . 5  wff  ( y  e.  b  <->  E. x  e.  a  ph )
1211, 2wal 1314 . . . 4  wff  A. y
( y  e.  b  <->  E. x  e.  a  ph )
1312, 8wex 1453 . . 3  wff  E. b A. y ( y  e.  b  <->  E. x  e.  a 
ph )
147, 13wi 4 . 2  wff  ( A. x  e.  a  E. y ph  ->  E. b A. y ( y  e.  b  <->  E. x  e.  a 
ph ) )
1514, 5wal 1314 1  wff  A. a
( A. x  e.  a  E. y ph  ->  E. b A. y
( y  e.  b  <->  E. x  e.  a  ph ) )
Colors of variables: wff set class
This axiom is referenced by:  strcoll2  13108
  Copyright terms: Public domain W3C validator