![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-pr | Unicode version |
Description: Define unordered pair of
classes. Definition 7.1 of [Quine] p. 48. They
are unordered, so ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-pr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | 1, 2 | cpr 3376 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1 | csn 3375 |
. . 3
![]() ![]() ![]() ![]() |
5 | 2 | csn 3375 |
. . 3
![]() ![]() ![]() ![]() |
6 | 4, 5 | cun 2915 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 6 | wceq 1243 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: dfsn2 3389 dfpr2 3394 ralprg 3421 rexprg 3422 disjpr2 3434 prcom 3446 preq1 3447 qdass 3467 qdassr 3468 tpidm12 3469 prprc1 3478 difprsn1 3503 diftpsn3 3505 snsspr1 3512 snsspr2 3513 prss 3520 prssg 3521 2ordpr 4249 xpsspw 4450 dmpropg 4793 rnpropg 4800 funprg 4949 funtp 4952 fntpg 4955 f1oprg 5168 fnimapr 5233 fpr 5345 fprg 5346 fmptpr 5355 fvpr1 5365 fvpr1g 5367 fvpr2g 5368 df2o3 6014 fzosplitprm1 9090 bdcpr 9991 |
Copyright terms: Public domain | W3C validator |