NFE Home 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
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cop 4561 . 2
4 vx . . . . . . 7
54cv 1641 . . . . . 6
6 vy . . . . . . . 8
76cv 1641 . . . . . . 7
87cphi 4562 . . . . . 6 Phi
95, 8wceq 1642 . . . . 5 Phi
109, 6, 1wrex 2615 . . . 4 Phi
1110, 4cab 2339 . . 3 Phi
12 c0c 4374 . . . . . . . 8 0c
1312csn 3737 . . . . . . 7 0c
148, 13cun 3207 . . . . . 6 Phi 0c
155, 14wceq 1642 . . . . 5 Phi 0c
1615, 6, 2wrex 2615 . . . 4 Phi 0c
1716, 4cab 2339 . . 3 Phi 0c
1811, 17cun 3207 . 2 Phi Phi 0c
193, 18wceq 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