![]() |
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 2798 | . . 3 ⊢ 𝐴 = 𝐴 | |
2 | 1 | orci 862 | . 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵) |
3 | elprg 4546 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵))) | |
4 | 2, 3 | mpbiri 261 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 844 = wceq 1538 ∈ wcel 2111 {cpr 4527 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-un 3886 df-sn 4526 df-pr 4528 |
This theorem is referenced by: prid2g 4657 prid1 4658 prnzg 4674 preq1b 4737 prel12g 4754 elpreqprb 4758 prproe 4798 opth1 5332 fr2nr 5497 fpr2g 6951 f1prex 7018 fveqf1o 7037 pw2f1olem 8604 hashprdifel 13755 gcdcllem3 15840 mgm2nsgrplem1 18075 mgm2nsgrplem2 18076 mgm2nsgrplem3 18077 sgrp2nmndlem1 18080 sgrp2rid2 18083 pmtrprfv 18573 pptbas 21613 coseq0negpitopi 25096 uhgr2edg 26998 umgrvad2edg 27003 uspgr2v1e2w 27041 usgr2v1e2w 27042 nbusgredgeu0 27158 nbusgrf1o0 27159 nb3grprlem1 27170 nb3grprlem2 27171 vtxduhgr0nedg 27282 1hegrvtxdg1 27297 1egrvtxdg1 27299 umgr2v2evd2 27317 vdegp1bi 27327 mptprop 30458 altgnsg 30841 cyc3genpmlem 30843 bj-prmoore 34530 ftc1anclem8 35137 kelac2 40009 pr2el1 40248 pr2eldif1 40253 fourierdlem54 42802 sge0pr 43033 imarnf1pr 43838 paireqne 44028 fmtnoprmfac2lem1 44083 1hegrlfgr 44360 |
Copyright terms: Public domain | W3C validator |