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

Axiom ax-strcoll 9442
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 𝑎(x 𝑎 yφ𝑏y(y 𝑏x 𝑎 φ))
Distinct variable groups:   𝑎,𝑏,x,y   φ,𝑎,𝑏
Allowed substitution hints:   φ(x,y)

Detailed syntax breakdown of Axiom ax-strcoll
StepHypRef Expression
1 wph . . . . 5 wff φ
2 vy . . . . 5 setvar y
31, 2wex 1378 . . . 4 wff yφ
4 vx . . . 4 setvar x
5 va . . . . 5 setvar 𝑎
65cv 1241 . . . 4 class 𝑎
73, 4, 6wral 2300 . . 3 wff x 𝑎 yφ
8 vb . . . . . . 7 setvar 𝑏
92, 8wel 1391 . . . . . 6 wff y 𝑏
101, 4, 6wrex 2301 . . . . . 6 wff x 𝑎 φ
119, 10wb 98 . . . . 5 wff (y 𝑏x 𝑎 φ)
1211, 2wal 1240 . . . 4 wff y(y 𝑏x 𝑎 φ)
1312, 8wex 1378 . . 3 wff 𝑏y(y 𝑏x 𝑎 φ)
147, 13wi 4 . 2 wff (x 𝑎 yφ𝑏y(y 𝑏x 𝑎 φ))
1514, 5wal 1240 1 wff 𝑎(x 𝑎 yφ𝑏y(y 𝑏x 𝑎 φ))
Colors of variables: wff set class
This axiom is referenced by:  strcoll2  9443
  Copyright terms: Public domain W3C validator