![]() |
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 3035 | . . 3 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | |
4 | elpri 4650 | . . . 4 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | |
5 | 4 | con3i 154 | . . 3 ⊢ (¬ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶}) |
6 | 3, 5 | sylbi 216 | . 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶}) |
7 | 1, 2, 6 | syl2anc 584 | 1 ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶}) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∨ wo 845 = wceq 1541 ∈ wcel 2106 ≠ wne 2940 {cpr 4630 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ne 2941 df-v 3476 df-un 3953 df-sn 4629 df-pr 4631 |
This theorem is referenced by: ord2eln012 8496 renfdisj 11273 sumtp 15694 pmtrprfv3 19321 logbgcd1irr 26296 perfectlem2 26730 nbupgrres 28618 usgr2pthlem 29017 eupth2lem3lem6 29483 cycpmco2 32287 cyc2fvx 32288 elrspunsn 32542 relogbzexpd 40835 dvrelog2b 40926 dvrelogpow2b 40928 aks4d1p1p4 40931 aks4d1p6 40941 mnuprdlem1 43021 mnuprdlem2 43022 perfectALTVlem2 46380 |
Copyright terms: Public domain | W3C validator |