![]() |
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 2733 | . . 3 ⊢ 𝐴 = 𝐴 | |
2 | 1 | orci 864 | . 2 ⊢ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵) |
3 | elprg 4648 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴, 𝐵} ↔ (𝐴 = 𝐴 ∨ 𝐴 = 𝐵))) | |
4 | 2, 3 | mpbiri 258 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 846 = wceq 1542 ∈ wcel 2107 {cpr 4629 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-un 3952 df-sn 4628 df-pr 4630 |
This theorem is referenced by: prid2g 4764 prid1 4765 prnzg 4781 preq1b 4846 prel12g 4863 elpreqprb 4867 prproe 4905 opth1 5474 fr2nr 5653 fpr2g 7208 f1prex 7277 fveqf1o 7296 pw2f1olem 9072 hashprdifel 14354 gcdcllem3 16438 mgm2nsgrplem1 18795 mgm2nsgrplem2 18796 mgm2nsgrplem3 18797 sgrp2nmndlem1 18800 sgrp2rid2 18803 pmtrprfv 19314 pptbas 22493 coseq0negpitopi 25995 uhgr2edg 28445 umgrvad2edg 28450 uspgr2v1e2w 28488 usgr2v1e2w 28489 nbusgredgeu0 28605 nbusgrf1o0 28606 nb3grprlem1 28617 nb3grprlem2 28618 vtxduhgr0nedg 28729 1hegrvtxdg1 28744 1egrvtxdg1 28746 umgr2v2evd2 28764 vdegp1bi 28774 mptprop 31898 altgnsg 32286 cyc3genpmlem 32288 elrspunsn 32505 bj-prmoore 35934 ftc1anclem8 36506 kelac2 41740 pr2el1 42233 pr2eldif1 42238 fourierdlem54 44811 sge0pr 45045 imarnf1pr 45925 paireqne 46114 fmtnoprmfac2lem1 46169 1hegrlfgr 46445 |
Copyright terms: Public domain | W3C validator |