![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > prid2g | Structured version Visualization version Unicode version |
Description: An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.) |
Ref | Expression |
---|---|
prid2g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prid1g 4046 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | prcom 4018 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl6eleq 2539 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1672 ax-4 1685 ax-5 1761 ax-6 1808 ax-7 1854 ax-10 1918 ax-11 1923 ax-12 1936 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1450 df-ex 1667 df-nf 1671 df-sb 1801 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-v 3014 df-un 3376 df-sn 3936 df-pr 3938 |
This theorem is referenced by: unisn2 4510 fr2nr 4789 fpr2g 6110 f1prex 6167 pw2f1olem 7662 hashprdifel 12568 gcdcllem3 14485 mgm2nsgrplem1 16662 mgm2nsgrplem2 16663 mgm2nsgrplem3 16664 sgrp2nmndlem1 16667 sgrp2rid2 16670 pmtrprfv 17104 m2detleib 19666 indistopon 20026 pptbas 20033 coseq0negpitopi 23469 usgra2edg 25120 nb3graprlem1 25190 nb3graprlem2 25191 2trllemF 25290 vdgr1b 25643 prsiga 28959 ftc1anclem8 32025 fourierdlem54 38080 prsal 38235 sge0pr 38294 imarnf1pr 39109 uhgr2edg 39390 uspgr2v1e2w 39427 usgr2v1e2w 39428 nb3grprlem1 39555 nb3grprlem2 39556 usgvad2edg 40047 |
Copyright terms: Public domain | W3C validator |