![]() |
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 3036 | . . 3 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | |
4 | elpri 4651 | . . . 4 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶)) | |
5 | 4 | con3i 154 | . . 3 ⊢ (¬ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶}) |
6 | 3, 5 | sylbi 216 | . 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶}) |
7 | 1, 2, 6 | syl2anc 585 | 1 ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶}) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 ∨ wo 846 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 {cpr 4631 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-v 3477 df-un 3954 df-sn 4630 df-pr 4632 |
This theorem is referenced by: ord2eln012 8497 renfdisj 11274 sumtp 15695 pmtrprfv3 19322 logbgcd1irr 26299 perfectlem2 26733 nbupgrres 28621 usgr2pthlem 29020 eupth2lem3lem6 29486 cycpmco2 32292 cyc2fvx 32293 elrspunsn 32547 relogbzexpd 40840 dvrelog2b 40931 dvrelogpow2b 40933 aks4d1p1p4 40936 aks4d1p6 40946 mnuprdlem1 43031 mnuprdlem2 43032 perfectALTVlem2 46390 |
Copyright terms: Public domain | W3C validator |