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 4580 | . 2 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | |
2 | 1 | ibi 268 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 841 = wceq 1528 ∈ wcel 2105 {cpr 4561 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3497 df-un 3940 df-sn 4560 df-pr 4562 |
This theorem is referenced by: nelpri 4586 nelprd 4588 tppreqb 4732 elpreqpr 4791 elpr2elpr 4793 prproe 4830 3elpr2eq 4831 opth1 5359 0nelop 5378 ftpg 6911 2oconcl 8119 cantnflem2 9142 eldju1st 9341 m1expcl2 13441 hash2pwpr 13824 bitsinv1lem 15780 prm23lt5 16141 fnpr2ob 16821 fvprif 16824 xpsfeq 16826 pmtrprfval 18546 m1expaddsub 18557 psgnprfval 18580 frgpuptinv 18828 frgpup3lem 18834 simpgnsgeqd 19154 2nsgsimpgd 19155 simpgnsgbid 19156 cnmsgnsubg 20651 zrhpsgnelbas 20668 mdetralt 21147 m2detleiblem1 21163 indiscld 21629 cnindis 21830 connclo 21953 txindis 22172 xpsxmetlem 22918 xpsmet 22921 ishl2 23902 recnprss 24431 recnperf 24432 dvlip2 24521 coseq0negpitopi 25018 pythag 25322 reasinsin 25401 scvxcvx 25491 perfectlem2 25734 lgslem4 25804 lgseisenlem2 25880 2lgsoddprmlem3 25918 usgredg4 26927 konigsberg 27964 ex-pr 28137 elpreq 30218 1neg1t1neg1 30400 tocyc01 30688 signswch 31731 kur14lem7 32357 poimirlem31 34805 ftc1anclem2 34850 wepwsolem 39522 relexp01min 39938 clsk1indlem1 40275 mnuprdlem1 40488 mnuprdlem2 40489 mnuprdlem3 40490 mnurndlem1 40497 ssrecnpr 40520 seff 40521 sblpnf 40522 expgrowthi 40545 dvconstbi 40546 sumpair 41172 refsum2cnlem1 41174 iooinlbub 41656 elprn1 41794 elprn2 41795 cncfiooicclem1 42056 dvmptconst 42079 dvmptidg 42081 dvmulcncf 42090 dvdivcncf 42092 elprneb 43145 perfectALTVlem2 43734 0dig2pr01 44568 prelrrx2b 44599 |
Copyright terms: Public domain | W3C validator |