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

Axiom ax-sscoll 11224
Description: Axiom scheme of subset 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-sscoll  |-  A. a A. b E. c A. z ( A. x  e.  a  E. y  e.  b  ph  ->  E. d  e.  c  A. y
( y  e.  d  <->  E. x  e.  a  ph ) )
Distinct variable groups:    a, b, c, d, x, y, z    ph, a, b, c, d
Allowed substitution hints:    ph( x, y, z)

Detailed syntax breakdown of Axiom ax-sscoll
StepHypRef Expression
1 wph . . . . . . . 8  wff  ph
2 vy . . . . . . . 8  setvar  y
3 vb . . . . . . . . 9  setvar  b
43cv 1284 . . . . . . . 8  class  b
51, 2, 4wrex 2354 . . . . . . 7  wff  E. y  e.  b  ph
6 vx . . . . . . 7  setvar  x
7 va . . . . . . . 8  setvar  a
87cv 1284 . . . . . . 7  class  a
95, 6, 8wral 2353 . . . . . 6  wff  A. x  e.  a  E. y  e.  b  ph
10 vd . . . . . . . . . 10  setvar  d
112, 10wel 1435 . . . . . . . . 9  wff  y  e.  d
121, 6, 8wrex 2354 . . . . . . . . 9  wff  E. x  e.  a  ph
1311, 12wb 103 . . . . . . . 8  wff  ( y  e.  d  <->  E. x  e.  a  ph )
1413, 2wal 1283 . . . . . . 7  wff  A. y
( y  e.  d  <->  E. x  e.  a  ph )
15 vc . . . . . . . 8  setvar  c
1615cv 1284 . . . . . . 7  class  c
1714, 10, 16wrex 2354 . . . . . 6  wff  E. d  e.  c  A. y
( y  e.  d  <->  E. x  e.  a  ph )
189, 17wi 4 . . . . 5  wff  ( A. x  e.  a  E. y  e.  b  ph  ->  E. d  e.  c 
A. y ( y  e.  d  <->  E. x  e.  a  ph ) )
19 vz . . . . 5  setvar  z
2018, 19wal 1283 . . . 4  wff  A. z
( A. x  e.  a  E. y  e.  b  ph  ->  E. d  e.  c  A. y
( y  e.  d  <->  E. x  e.  a  ph ) )
2120, 15wex 1422 . . 3  wff  E. c A. z ( A. x  e.  a  E. y  e.  b  ph  ->  E. d  e.  c  A. y
( y  e.  d  <->  E. x  e.  a  ph ) )
2221, 3wal 1283 . 2  wff  A. b E. c A. z ( A. x  e.  a  E. y  e.  b 
ph  ->  E. d  e.  c 
A. y ( y  e.  d  <->  E. x  e.  a  ph ) )
2322, 7wal 1283 1  wff  A. a A. b E. c A. z ( A. x  e.  a  E. y  e.  b  ph  ->  E. d  e.  c  A. y
( y  e.  d  <->  E. x  e.  a  ph ) )
Colors of variables: wff set class
This axiom is referenced by:  sscoll2  11225
  Copyright terms: Public domain W3C validator