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

Definition df-op 4566
 Description: Define the type-level ordered pair. Definition from [Rosser] p. 281.
Assertion
Ref Expression
df-op A, B = ({x y A x = Phi y} ∪ {x y B x = ( Phi y ∪ {0c})})
Distinct variable groups:   x,y,A   x,B,y

Detailed syntax breakdown of Definition df-op
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2cop 4561 . 2 class A, B
4 vx . . . . . . 7 set x
54cv 1641 . . . . . 6 class x
6 vy . . . . . . . 8 set y
76cv 1641 . . . . . . 7 class y
87cphi 4562 . . . . . 6 class Phi y
95, 8wceq 1642 . . . . 5 wff x = Phi y
109, 6, 1wrex 2615 . . . 4 wff y A x = Phi y
1110, 4cab 2339 . . 3 class {x y A x = Phi y}
12 c0c 4374 . . . . . . . 8 class 0c
1312csn 3737 . . . . . . 7 class {0c}
148, 13cun 3207 . . . . . 6 class ( Phi y ∪ {0c})
155, 14wceq 1642 . . . . 5 wff x = ( Phi y ∪ {0c})
1615, 6, 2wrex 2615 . . . 4 wff y B x = ( Phi y ∪ {0c})
1716, 4cab 2339 . . 3 class {x y B x = ( Phi y ∪ {0c})}
1811, 17cun 3207 . 2 class ({x y A x = Phi y} ∪ {x y B x = ( Phi y ∪ {0c})})
193, 18wceq 1642 1 wff A, B = ({x y A x = Phi y} ∪ {x y B x = ( Phi y ∪ {0c})})
 Colors of variables: wff set class This definition is referenced by:  dfop2  4575  proj1op  4598  proj2op  4599  nfop  4602  eqop  4609  dfswap2  4733
 Copyright terms: Public domain W3C validator