![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elpr | GIF version |
Description: A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
Ref | Expression |
---|---|
elpr.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
elpr | ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpr.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | elprg 3442 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 103 ∨ wo 662 = wceq 1285 ∈ wcel 1434 Vcvv 2612 {cpr 3423 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-v 2614 df-un 2988 df-sn 3428 df-pr 3429 |
This theorem is referenced by: prmg 3535 difprsnss 3549 preqr1 3586 preq12b 3588 prel12 3589 pwprss 3623 pwtpss 3624 unipr 3641 intpr 3694 zfpair2 4001 elop 4022 ordtri2or2exmidlem 4305 onsucelsucexmidlem 4308 en2lp 4333 reg3exmidlemwe 4357 xpsspw 4508 acexmidlem2 5588 2oconcl 6135 exmidpw 6551 renfdisj 7449 fzpr 9384 maxabslemval 10468 isprm2 10879 bj-zfpair2 11144 |
Copyright terms: Public domain | W3C validator |