![]() |
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 3627 | . 2 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | |
2 | 1 | ibi 176 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 709 = wceq 1364 ∈ wcel 2160 {cpr 3608 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-un 3148 df-sn 3613 df-pr 3614 |
This theorem is referenced by: nelpri 3631 nelprd 3633 opth1 4254 0nelop 4266 ontr2exmid 4542 onintexmid 4590 reg3exmidlemwe 4596 funtpg 5286 ftpg 5721 acexmidlemcase 5892 2oconcl 6465 el2oss1o 6469 pw2f1odclem 6863 en2eqpr 6936 eldju1st 7101 nninfisol 7162 finomni 7169 exmidomniim 7170 ismkvnex 7184 nninfwlpoimlemginf 7205 exmidonfinlem 7223 exmidfodomrlemr 7232 exmidfodomrlemrALT 7233 exmidaclem 7238 sup3exmid 8945 m1expcl2 10576 maxleim 11249 maxleast 11257 zmaxcl 11268 minmax 11273 xrmaxleim 11287 xrmaxaddlem 11303 xrminmax 11308 prm23lt5 12298 unct 12496 fnpr2ob 12819 fvprif 12822 xpsfeq 12824 qtopbas 14499 limcimolemlt 14610 recnprss 14633 coseq0negpitopi 14734 lgslem4 14882 lgseisenlem2 14929 2lgsoddprmlem3 14937 012of 15224 2o01f 15225 nninfalllem1 15236 nninfall 15237 nninfsellemqall 15243 nninfomnilem 15246 trilpolemclim 15263 trilpolemcl 15264 trilpolemisumle 15265 trilpolemeq1 15267 trilpolemlt1 15268 iswomni0 15278 nconstwlpolemgt0 15291 nconstwlpolem 15292 |
Copyright terms: Public domain | W3C validator |