| 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 2765 | . . 3 ⊢ 𝐴 = 𝐴 | |
| 2 | 1 | orci 878 | . 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵) |
| 3 | elprg 4608 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵))) | |
| 4 | 2, 3 | mpbiri 261 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵}) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∨ wo 860 = wceq 1563 ∈ wcel 2145 {cpr 4587 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-tru 1566 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-v 3459 df-un 3912 df-sn 4586 df-pr 4588 |
| This theorem is referenced by: prid2g 4723 prid1 4724 prnzg 4740 preq1b 4807 prel12g 4825 elpreqprb 4829 prproe 4866 opth1 5448 fr2nr 5629 fpr2g 7199 f1prex 7272 fveqf1o 7290 fvf1pr 7295 pw2f1olem 9057 hashprdifel 14425 gcdcllem3 16549 mgm2nsgrplem1 18970 mgm2nsgrplem2 18971 mgm2nsgrplem3 18972 sgrp2nmndlem1 18975 sgrp2rid2 18978 pmtrprfv 19514 pptbas 23126 coseq0negpitopi 26626 uhgr2edg 29467 umgrvad2edg 29472 uspgr2v1e2w 29510 usgr2v1e2w 29511 nbusgredgeu0 29627 nbusgrf1o0 29628 nb3grprlem1 29639 nb3grprlem2 29640 vtxduhgr0nedg 29751 1hegrvtxdg1 29766 1egrvtxdg1 29768 umgr2v2evd2 29786 vdegp1bi 29796 mptprop 32955 altgnsg 33382 cyc3genpmlem 33384 elrspunsn 33653 esplyfval1 33880 bj-prmoore 37617 ftc1anclem8 38211 kelac2 43654 pr2el1 44137 pr2eldif1 44142 fourierdlem54 46732 sge0pr 46966 imarnf1pr 47874 paireqne 48115 fmtnoprmfac2lem1 48173 grlimprclnbgr 48616 grlimprclnbgredg 48617 1hegrlfgr 48752 fucoppcffth 50040 termc2 50147 uobeqterm 50175 2arwcatlem4 50227 incat 50230 |
| Copyright terms: Public domain | W3C validator |