NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-co GIF version

Definition df-co 4726
Description: Define the composition of two classes. (Contributed by SF, 5-Jan-2015.)
Assertion
Ref Expression
df-co (A B) = {x, y z(xBz zAy)}
Distinct variable groups:   x,A,y,z   x,B,y,z

Detailed syntax breakdown of Definition df-co
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2ccom 4721 . 2 class (A B)
4 vx . . . . . . 7 setvar x
54cv 1641 . . . . . 6 class x
6 vz . . . . . . 7 setvar z
76cv 1641 . . . . . 6 class z
85, 7, 2wbr 4639 . . . . 5 wff xBz
9 vy . . . . . . 7 setvar y
109cv 1641 . . . . . 6 class y
117, 10, 1wbr 4639 . . . . 5 wff zAy
128, 11wa 358 . . . 4 wff (xBz zAy)
1312, 6wex 1541 . . 3 wff z(xBz zAy)
1413, 4, 9copab 4622 . 2 class {x, y z(xBz zAy)}
153, 14wceq 1642 1 wff (A B) = {x, y z(xBz zAy)}
Colors of variables: wff setvar class
This definition is referenced by:  dfco1  4748  coss1  4872  coss2  4873  nfco  4882  brco  4883  cnvco  4894  coundi  5082  coundir  5083  cores  5084  df2nd2  5111  funco  5142  composeex  5820
  Copyright terms: Public domain W3C validator