![]() |
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 4389 | . 2 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | |
2 | 1 | ibi 259 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 874 = wceq 1653 ∈ wcel 2157 {cpr 4370 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-v 3387 df-un 3774 df-sn 4369 df-pr 4371 |
This theorem is referenced by: nelpri 4393 nelprd 4395 tppreqb 4524 elpreqpr 4587 elpr2elpr 4589 prproe 4626 3elpr2eq 4627 opth1 5134 0nelop 5150 ftpg 6651 2oconcl 7823 cantnflem2 8837 eldju1st 9035 m1expcl2 13136 hash2pwpr 13507 bitsinv1lem 15498 prm23lt5 15852 xpscfv 16537 xpsfeq 16539 pmtrprfval 18219 m1expaddsub 18231 psgnprfval 18254 frgpuptinv 18499 frgpup3lem 18505 cnmsgnsubg 20244 zrhpsgnelbas 20262 mdetralt 20740 m2detleiblem1 20756 indiscld 21224 cnindis 21425 connclo 21547 txindis 21766 xpsxmetlem 22512 xpsmet 22515 ishl2 23496 recnprss 24009 recnperf 24010 dvlip2 24099 coseq0negpitopi 24597 pythag 24899 reasinsin 24975 scvxcvx 25064 perfectlem2 25307 lgslem4 25377 lgseisenlem2 25453 2lgsoddprmlem3 25491 usgredg4 26450 konigsberg 27604 ex-pr 27815 elpreq 29878 1neg1t1neg1 30032 signswch 31156 kur14lem7 31711 poimirlem31 33929 ftc1anclem2 33974 wepwsolem 38397 relexp01min 38788 clsk1indlem1 39125 ssrecnpr 39289 seff 39290 sblpnf 39291 expgrowthi 39314 dvconstbi 39315 sumpair 39954 refsum2cnlem1 39956 iooinlbub 40471 elprn1 40609 elprn2 40610 cncfiooicclem1 40850 dvmptconst 40873 dvmptidg 40875 dvmulcncf 40884 dvdivcncf 40886 elprneb 41917 perfectALTVlem2 42413 0dig2pr01 43203 |
Copyright terms: Public domain | W3C validator |