![]() |
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 4612 | . 2 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | |
2 | 1 | ibi 267 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 846 = wceq 1542 ∈ wcel 2107 {cpr 4593 |
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 2708 |
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 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-un 3920 df-sn 4592 df-pr 4594 |
This theorem is referenced by: nelpri 4620 nelprd 4622 tppreqb 4770 elpreqpr 4829 elpr2elpr 4831 prproe 4868 3elpr2eq 4869 opth1 5437 0nelop 5458 ftpg 7107 2oconcl 8454 cantnflem2 9633 eldju1st 9866 m1expcl2 13998 hash2pwpr 14382 bitsinv1lem 16328 prm23lt5 16693 fnpr2ob 17447 fvprif 17450 xpsfeq 17452 pmtrprfval 19276 m1expaddsub 19287 psgnprfval 19310 frgpuptinv 19560 frgpup3lem 19566 simpgnsgeqd 19887 2nsgsimpgd 19888 simpgnsgbid 19889 cnmsgnsubg 20997 zrhpsgnelbas 21014 mdetralt 21973 m2detleiblem1 21989 indiscld 22458 cnindis 22659 connclo 22782 txindis 23001 xpsxmetlem 23748 xpsmet 23751 ishl2 24750 recnprss 25284 recnperf 25285 dvlip2 25375 coseq0negpitopi 25876 pythag 26183 reasinsin 26262 scvxcvx 26351 perfectlem2 26594 lgslem4 26664 lgseisenlem2 26740 2lgsoddprmlem3 26778 usgredg4 28207 konigsberg 29243 ex-pr 29416 elpreq 31499 1neg1t1neg1 31696 tocyc01 32009 signswch 33213 kur14lem7 33846 poimirlem31 36138 ftc1anclem2 36181 wepwsolem 41398 omabs2 41696 omcl3g 41698 relexp01min 42059 clsk1indlem1 42391 mnuprdlem1 42626 mnuprdlem2 42627 mnuprdlem3 42628 mnurndlem1 42635 ssrecnpr 42662 seff 42663 sblpnf 42664 expgrowthi 42687 dvconstbi 42688 sumpair 43314 refsum2cnlem1 43316 iooinlbub 43813 elprn1 43948 elprn2 43949 cncfiooicclem1 44208 dvmptconst 44230 dvmptidg 44232 dvmulcncf 44240 dvdivcncf 44242 elprneb 45337 perfectALTVlem2 45988 0dig2pr01 46770 prelrrx2b 46874 setc2othin 47150 |
Copyright terms: Public domain | W3C validator |