![]() |
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 4785 | . 2 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵, 𝐴}) | |
2 | prcom 4757 | . 2 ⊢ {𝐵, 𝐴} = {𝐴, 𝐵} | |
3 | 1, 2 | eleqtrdi 2854 | 1 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐴, 𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2108 {cpr 4650 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2711 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-tru 1540 df-ex 1778 df-sb 2065 df-clab 2718 df-cleq 2732 df-clel 2819 df-v 3490 df-un 3981 df-sn 4649 df-pr 4651 |
This theorem is referenced by: prel12g 4888 prproe 4929 unisn2 5330 fr2nr 5677 fpr2g 7248 f1prex 7320 fvf1pr 7343 pw2f1olem 9142 hashprdifel 14447 gcdcllem3 16547 mgm2nsgrplem1 18953 mgm2nsgrplem2 18954 mgm2nsgrplem3 18955 sgrp2nmndlem1 18958 sgrp2rid2 18961 pmtrprfv 19495 m2detleib 22658 indistopon 23029 pptbas 23036 coseq0negpitopi 26563 uhgr2edg 29243 umgrvad2edg 29248 uspgr2v1e2w 29286 usgr2v1e2w 29287 nb3grprlem1 29415 nb3grprlem2 29416 1hegrvtxdg1 29543 cyc3genpmlem 33144 elrspunsn 33422 prsiga 34095 bj-prmoore 37081 ftc1anclem8 37660 pr2el2 43513 pr2eldif2 43517 fourierdlem54 46081 prsal 46239 sge0pr 46315 imarnf1pr 47197 paireqne 47385 1hegrlfgr 47855 lubprlem 48642 |
Copyright terms: Public domain | W3C validator |