![]() |
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 4418 | . 2 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | |
2 | 1 | ibi 259 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 878 = wceq 1656 ∈ wcel 2164 {cpr 4399 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-v 3416 df-un 3803 df-sn 4398 df-pr 4400 |
This theorem is referenced by: nelpri 4422 nelprd 4424 tppreqb 4554 elpreqpr 4617 elpr2elpr 4619 prproe 4656 3elpr2eq 4657 opth1 5164 0nelop 5180 ftpg 6674 2oconcl 7850 cantnflem2 8864 eldju1st 9062 m1expcl2 13176 hash2pwpr 13547 bitsinv1lem 15536 prm23lt5 15890 xpscfv 16575 xpsfeq 16577 pmtrprfval 18257 m1expaddsub 18269 psgnprfval 18292 frgpuptinv 18537 frgpup3lem 18543 cnmsgnsubg 20282 zrhpsgnelbas 20300 mdetralt 20782 m2detleiblem1 20798 indiscld 21266 cnindis 21467 connclo 21589 txindis 21808 xpsxmetlem 22554 xpsmet 22557 ishl2 23538 recnprss 24067 recnperf 24068 dvlip2 24157 coseq0negpitopi 24655 pythag 24957 reasinsin 25036 scvxcvx 25125 perfectlem2 25368 lgslem4 25438 lgseisenlem2 25514 2lgsoddprmlem3 25552 usgredg4 26513 konigsberg 27625 ex-pr 27834 elpreq 29897 1neg1t1neg1 30050 signswch 31174 kur14lem7 31729 poimirlem31 33977 ftc1anclem2 34022 wepwsolem 38448 relexp01min 38839 clsk1indlem1 39176 ssrecnpr 39340 seff 39341 sblpnf 39342 expgrowthi 39365 dvconstbi 39366 sumpair 40005 refsum2cnlem1 40007 iooinlbub 40515 elprn1 40653 elprn2 40654 cncfiooicclem1 40894 dvmptconst 40917 dvmptidg 40919 dvmulcncf 40928 dvdivcncf 40930 elprneb 41958 perfectALTVlem2 42454 0dig2pr01 43244 |
Copyright terms: Public domain | W3C validator |