![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nelprd | Structured version Visualization version GIF version |
Description: If an element doesn't match the items in an unordered pair, it is not in the unordered pair, deduction version. (Contributed by Alexander van der Vekens, 25-Jan-2018.) |
Ref | Expression |
---|---|
nelprd.1 | ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
nelprd.2 | ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
Ref | Expression |
---|---|
nelprd | ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nelprd.1 | . 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵) | |
2 | nelprd.2 | . 2 ⊢ (𝜑 → 𝐴 ≠ 𝐶) | |
3 | neanior 3033 | . . 3 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | |
4 | elpri 4651 | . . . 4 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | |
5 | 4 | con3i 154 | . . 3 ⊢ (¬ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶}) |
6 | 3, 5 | sylbi 216 | . 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶}) |
7 | 1, 2, 6 | syl2anc 582 | 1 ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶}) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 394 ∨ wo 843 = wceq 1539 ∈ wcel 2104 ≠ wne 2938 {cpr 4631 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-ne 2939 df-v 3474 df-un 3954 df-sn 4630 df-pr 4632 |
This theorem is referenced by: ord2eln012 8501 renfdisj 11280 sumtp 15701 pmtrprfv3 19365 logbgcd1irr 26533 perfectlem2 26967 nbupgrres 28886 usgr2pthlem 29285 eupth2lem3lem6 29751 cycpmco2 32560 cyc2fvx 32561 elrspunsn 32819 relogbzexpd 41148 dvrelog2b 41239 dvrelogpow2b 41241 aks4d1p1p4 41244 aks4d1p6 41254 mnuprdlem1 43335 mnuprdlem2 43336 perfectALTVlem2 46690 |
Copyright terms: Public domain | W3C validator |