![]() |
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 3619 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1 | csn 3618 |
. . 3
![]() ![]() ![]() ![]() |
5 | 2 | csn 3618 |
. . 3
![]() ![]() ![]() ![]() |
6 | 4, 5 | cun 3151 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 6 | wceq 1364 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: dfsn2 3632 dfpr2 3637 ralprg 3669 rexprg 3670 disjpr2 3682 prcom 3694 preq1 3695 qdass 3715 qdassr 3716 tpidm12 3717 prprc1 3726 difprsn1 3757 diftpsn3 3759 difpr 3760 snsspr1 3766 snsspr2 3767 prss 3774 prssg 3775 iunxprg 3993 2ordpr 4556 xpsspw 4771 dmpropg 5138 rnpropg 5145 funprg 5304 funtp 5307 fntpg 5310 f1oprg 5544 fnimapr 5617 fpr 5740 fprg 5741 fmptpr 5750 fvpr1 5762 fvpr1g 5764 fvpr2g 5765 df2o3 6483 enpr2d 6871 unfiexmid 6974 prfidisj 6983 pr2nelem 7251 xp2dju 7275 fzosplitprm1 10301 hashprg 10879 sumpr 11556 strle2g 12725 bdcpr 15363 |
Copyright terms: Public domain | W3C validator |