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

---

Definition df-op 4566

Description: Define the type-level ordered pair. Definition from [Rosser] p. 281. (Contributed by SF, 3-Feb-2015.)

Assertion

Ref	Expression
df-op	Phi Phi 0c

Distinct variable groups:   ,,   ,,

---

Detailed syntax breakdown of Definition df-op

Step	Hyp	Ref	Expression
1		cA	. . 3
2		cB	. . 3
3	1, 2	cop 4561	. 2
4		vx	. . . . . . 7
5	4	cv 1641	. . . . . 6
6		vy	. . . . . . . 8
7	6	cv 1641	. . . . . . 7
8	7	cphi 4562	. . . . . 6 Phi
9	5, 8	wceq 1642	. . . . 5 Phi
10	9, 6, 1	wrex 2615	. . . 4 Phi
11	10, 4	cab 2339	. . 3 Phi
12		c0c 4374	. . . . . . . 8 0c
13	12	csn 3737	. . . . . . 7 0c
14	8, 13	cun 3207	. . . . . 6 Phi 0c
15	5, 14	wceq 1642	. . . . 5 Phi 0c
16	15, 6, 2	wrex 2615	. . . 4 Phi 0c
17	16, 4	cab 2339	. . 3 Phi 0c
18	11, 17	cun 3207	. 2 Phi Phi 0c
19	3, 18	wceq 1642	1 Phi Phi 0c

Colors of variables: wff setvar class

This definition is referenced by:  dfop2  4575  proj1op  4600  proj2op  4601  nfop  4604  eqop  4611  opeq  4619  dfswap2  4741

Copyright terms: Public domain

W3C validator