![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > prid2g | Structured version Visualization version GIF 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 4327 | . 2 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵, 𝐴}) | |
2 | prcom 4299 | . 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵} | |
3 | 1, 2 | syl6eleq 2740 | 1 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐴, 𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2030 {cpr 4212 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-un 3612 df-sn 4211 df-pr 4213 |
This theorem is referenced by: prproe 4466 unisn2 4827 fr2nr 5121 fpr2g 6516 f1prex 6579 pw2f1olem 8105 hashprdifel 13224 gcdcllem3 15270 mgm2nsgrplem1 17452 mgm2nsgrplem2 17453 mgm2nsgrplem3 17454 sgrp2nmndlem1 17457 sgrp2rid2 17460 pmtrprfv 17919 m2detleib 20485 indistopon 20853 pptbas 20860 coseq0negpitopi 24300 uhgr2edg 26145 umgrvad2edg 26150 uspgr2v1e2w 26188 usgr2v1e2w 26189 nb3grprlem1 26326 nb3grprlem2 26327 1hegrvtxdg1 26459 prsiga 30322 ftc1anclem8 33622 fourierdlem54 40695 prsal 40856 sge0pr 40929 imarnf1pr 41624 1hegrlfgr 42038 |
Copyright terms: Public domain | W3C validator |