Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > prid1g | Structured version Visualization version GIF version |
Description: An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.) |
Ref | Expression |
---|---|
prid1g | ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2818 | . . 3 ⊢ 𝐴 = 𝐴 | |
2 | 1 | orci 859 | . 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵) |
3 | elprg 4578 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵))) | |
4 | 2, 3 | mpbiri 259 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 841 = wceq 1528 ∈ wcel 2105 {cpr 4559 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-un 3938 df-sn 4558 df-pr 4560 |
This theorem is referenced by: prid2g 4689 prid1 4690 prnzg 4705 preq1b 4769 prel12g 4786 elpreqprb 4790 prproe 4828 opth1 5358 fr2nr 5526 fpr2g 6965 f1prex 7031 fveqf1o 7049 pw2f1olem 8609 hashprdifel 13747 gcdcllem3 15838 mgm2nsgrplem1 18021 mgm2nsgrplem2 18022 mgm2nsgrplem3 18023 sgrp2nmndlem1 18026 sgrp2rid2 18029 pmtrprfv 18510 pptbas 21544 coseq0negpitopi 25016 uhgr2edg 26917 umgrvad2edg 26922 uspgr2v1e2w 26960 usgr2v1e2w 26961 nbusgredgeu0 27077 nbusgrf1o0 27078 nb3grprlem1 27089 nb3grprlem2 27090 vtxduhgr0nedg 27201 1hegrvtxdg1 27216 1egrvtxdg1 27218 umgr2v2evd2 27236 vdegp1bi 27246 mptprop 30360 altgnsg 30718 cyc3genpmlem 30720 ftc1anclem8 34855 kelac2 39543 pr2el1 39786 pr2eldif1 39791 fourierdlem54 42322 sge0pr 42553 imarnf1pr 43358 paireqne 43550 fmtnoprmfac2lem1 43605 1hegrlfgr 43884 |
Copyright terms: Public domain | W3C validator |