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 2738 | . . 3 ⊢ 𝐴 = 𝐴 | |
2 | 1 | orci 864 | . 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵) |
3 | elprg 4534 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵))) | |
4 | 2, 3 | mpbiri 261 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 846 = wceq 1542 ∈ wcel 2113 {cpr 4515 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3399 df-un 3846 df-sn 4514 df-pr 4516 |
This theorem is referenced by: prid2g 4649 prid1 4650 prnzg 4666 preq1b 4729 prel12g 4746 elpreqprb 4750 prproe 4791 opth1 5330 fr2nr 5497 fpr2g 6978 f1prex 7045 fveqf1o 7064 pw2f1olem 8663 hashprdifel 13844 gcdcllem3 15937 mgm2nsgrplem1 18192 mgm2nsgrplem2 18193 mgm2nsgrplem3 18194 sgrp2nmndlem1 18197 sgrp2rid2 18200 pmtrprfv 18692 pptbas 21752 coseq0negpitopi 25240 uhgr2edg 27142 umgrvad2edg 27147 uspgr2v1e2w 27185 usgr2v1e2w 27186 nbusgredgeu0 27302 nbusgrf1o0 27303 nb3grprlem1 27314 nb3grprlem2 27315 vtxduhgr0nedg 27426 1hegrvtxdg1 27441 1egrvtxdg1 27443 umgr2v2evd2 27461 vdegp1bi 27471 mptprop 30598 altgnsg 30985 cyc3genpmlem 30987 bj-prmoore 34896 ftc1anclem8 35469 kelac2 40446 pr2el1 40685 pr2eldif1 40690 fourierdlem54 43227 sge0pr 43458 imarnf1pr 44291 paireqne 44481 fmtnoprmfac2lem1 44536 1hegrlfgr 44812 |
Copyright terms: Public domain | W3C validator |