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 4144 | . 2 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | |
2 | 1 | ibi 255 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 382 = wceq 1475 ∈ wcel 1977 {cpr 4127 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-un 3545 df-sn 4126 df-pr 4128 |
This theorem is referenced by: elpr2OLD 4148 nelpri 4149 nelprd 4151 tppreqb 4277 elpreqpr 4334 elpr2elpr 4336 opth1 4870 0nelop 4886 funtpgOLD 5857 ftpg 6328 2oconcl 7470 cantnflem2 8470 m1expcl2 12744 hash2pwpr 13115 bitsinv1lem 15001 prm23lt5 15357 xpscfv 16045 xpsfeq 16047 pmtrprfval 17730 m1expaddsub 17741 psgnprfval 17764 frgpuptinv 18007 frgpup3lem 18013 cnmsgnsubg 19742 zrhpsgnelbas 19759 mdetralt 20233 m2detleiblem1 20249 indiscld 20705 cnindis 20906 conclo 21028 txindis 21247 xpsxmetlem 21994 xpsmet 21997 ishl2 22974 recnprss 23474 recnperf 23475 dvlip2 23562 coseq0negpitopi 24059 pythag 24347 reasinsin 24423 scvxcvx 24512 perfectlem2 24755 lgslem4 24825 lgseisenlem2 24901 2lgsoddprmlem3 24939 usgraedg4 25916 cusgrares 26001 2pthlem2 26126 vdgr1a 26433 konigsberg 26514 ex-pr 26679 elpreq 28744 1neg1t1neg1 28902 signswch 29964 kur14lem7 30448 poimirlem31 32610 ftc1anclem2 32656 wepwsolem 36630 relexp01min 37024 clsk1indlem1 37363 ssrecnpr 37529 seff 37530 sblpnf 37531 expgrowthi 37554 dvconstbi 37555 sumpair 38217 refsum2cnlem1 38219 iooinlbub 38570 elprn1 38700 elprn2 38701 cncfiooicclem1 38779 dvmptconst 38803 dvmptidg 38805 dvmulcncf 38815 dvdivcncf 38817 elprneb 39939 perfectALTVlem2 40165 usgredg4 40444 konigsberg-av 41427 0dig2pr01 42202 |
Copyright terms: Public domain | W3C validator |