![]() |
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 3594 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1 | csn 3593 |
. . 3
![]() ![]() ![]() ![]() |
5 | 2 | csn 3593 |
. . 3
![]() ![]() ![]() ![]() |
6 | 4, 5 | cun 3128 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 6 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: dfsn2 3607 dfpr2 3612 ralprg 3644 rexprg 3645 disjpr2 3657 prcom 3669 preq1 3670 qdass 3690 qdassr 3691 tpidm12 3692 prprc1 3701 difprsn1 3732 diftpsn3 3734 difpr 3735 snsspr1 3741 snsspr2 3742 prss 3749 prssg 3750 iunxprg 3968 2ordpr 4524 xpsspw 4739 dmpropg 5102 rnpropg 5109 funprg 5267 funtp 5270 fntpg 5273 f1oprg 5506 fnimapr 5577 fpr 5699 fprg 5700 fmptpr 5709 fvpr1 5721 fvpr1g 5723 fvpr2g 5724 df2o3 6431 enpr2d 6817 unfiexmid 6917 prfidisj 6926 pr2nelem 7190 xp2dju 7214 fzosplitprm1 10234 hashprg 10788 sumpr 11421 strle2g 12566 bdcpr 14626 |
Copyright terms: Public domain | W3C validator |