Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elpri | 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 3590 | . 2 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | |
2 | 1 | ibi 175 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 698 = wceq 1342 ∈ wcel 2135 {cpr 3571 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 df-un 3115 df-sn 3576 df-pr 3577 |
This theorem is referenced by: nelpri 3594 nelprd 3596 opth1 4208 0nelop 4220 ontr2exmid 4496 onintexmid 4544 reg3exmidlemwe 4550 funtpg 5233 ftpg 5663 acexmidlemcase 5831 2oconcl 6398 el2oss1o 6402 en2eqpr 6864 eldju1st 7027 nninfisol 7088 finomni 7095 exmidomniim 7096 ismkvnex 7110 exmidonfinlem 7140 exmidfodomrlemr 7149 exmidfodomrlemrALT 7150 exmidaclem 7155 sup3exmid 8843 m1expcl2 10467 maxleim 11133 maxleast 11141 zmaxcl 11152 minmax 11157 xrmaxleim 11171 xrmaxaddlem 11187 xrminmax 11192 prm23lt5 12172 unct 12312 qtopbas 13063 limcimolemlt 13174 recnprss 13197 coseq0negpitopi 13298 012of 13709 2o01f 13710 nninfalllem1 13722 nninfall 13723 nninfsellemqall 13729 nninfomnilem 13732 trilpolemclim 13749 trilpolemcl 13750 trilpolemisumle 13751 trilpolemeq1 13753 trilpolemlt1 13754 iswomni0 13764 nconstwlpolemgt0 13776 nconstwlpolem 13777 |
Copyright terms: Public domain | W3C validator |