Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elpri | Structured version Visualization version GIF version |
Description: If a class is an element of a pair, then it is one of the two paired elements. (Contributed by Scott Fenton, 1-Apr-2011.) |
Ref | Expression |
---|---|
elpri | ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elprg 4579 | . 2 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | |
2 | 1 | ibi 270 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 847 = wceq 1543 ∈ wcel 2112 {cpr 4560 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-sb 2073 df-clab 2717 df-cleq 2731 df-clel 2818 df-v 3425 df-un 3888 df-sn 4559 df-pr 4561 |
This theorem is referenced by: nelpri 4587 nelprd 4589 tppreqb 4735 elpreqpr 4794 elpr2elpr 4796 prproe 4834 3elpr2eq 4835 opth1 5376 0nelop 5396 ftpg 6993 2oconcl 8254 cantnflem2 9335 eldju1st 9569 m1expcl2 13689 hash2pwpr 14075 bitsinv1lem 16033 prm23lt5 16400 fnpr2ob 17096 fvprif 17099 xpsfeq 17101 pmtrprfval 18912 m1expaddsub 18923 psgnprfval 18946 frgpuptinv 19194 frgpup3lem 19200 simpgnsgeqd 19521 2nsgsimpgd 19522 simpgnsgbid 19523 cnmsgnsubg 20572 zrhpsgnelbas 20589 mdetralt 21537 m2detleiblem1 21553 indiscld 22020 cnindis 22221 connclo 22344 txindis 22563 xpsxmetlem 23309 xpsmet 23312 ishl2 24299 recnprss 24833 recnperf 24834 dvlip2 24924 coseq0negpitopi 25425 pythag 25732 reasinsin 25811 scvxcvx 25900 perfectlem2 26143 lgslem4 26213 lgseisenlem2 26289 2lgsoddprmlem3 26327 usgredg4 27337 konigsberg 28372 ex-pr 28545 elpreq 30629 1neg1t1neg1 30824 tocyc01 31136 signswch 32284 kur14lem7 32918 poimirlem31 35582 ftc1anclem2 35625 wepwsolem 40618 relexp01min 41046 clsk1indlem1 41380 mnuprdlem1 41611 mnuprdlem2 41612 mnuprdlem3 41613 mnurndlem1 41620 ssrecnpr 41647 seff 41648 sblpnf 41649 expgrowthi 41672 dvconstbi 41673 sumpair 42299 refsum2cnlem1 42301 iooinlbub 42760 elprn1 42895 elprn2 42896 cncfiooicclem1 43155 dvmptconst 43177 dvmptidg 43179 dvmulcncf 43187 dvdivcncf 43189 elprneb 44241 perfectALTVlem2 44893 0dig2pr01 45675 prelrrx2b 45779 setc2othin 46056 |
Copyright terms: Public domain | W3C validator |