| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > neleqtrrd | Structured version Visualization version GIF version | ||
| Description: If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017.) (Proof shortened by Wolf Lammen, 13-Nov-2019.) |
| Ref | Expression |
|---|---|
| neleqtrrd.1 | ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵) |
| neleqtrrd.2 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Ref | Expression |
|---|---|
| neleqtrrd | ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | neleqtrrd.1 | . 2 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐵) | |
| 2 | neleqtrrd.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 3 | 2 | eqcomd 2747 | . 2 ⊢ (𝜑 → 𝐵 = 𝐴) |
| 4 | 1, 3 | neleqtrd 2863 | 1 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1548 ∈ wcel 2121 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-ext 2713 |
| This theorem depends on definitions: df-bi 209 df-an 398 df-ex 1788 df-cleq 2733 df-clel 2816 |
| This theorem is referenced by: csbxp 5722 omopth2 8513 wrdlndm 14487 mreexd 17603 mreexmrid 17604 psgnunilem2 19465 lspindp4 21134 lsppratlem3 21146 frlmlbs 21776 mdetralt 22595 lebnumlem1 24950 mideulem2 28824 opphllem 28825 structiedg0val 29113 snstriedgval 29129 1hevtxdg0 29596 cyc2fvx 33219 cyc3co2 33225 elrgspnlem4 33330 lindssn 33465 evlextv 33738 qqhval2lem 34177 qqhf 34182 unbdqndv1 36829 lindsenlbs 37997 mapdindp2 42228 mapdindp4 42230 mapdh6dN 42246 hdmap1l6d 42320 tfsconcatb0 43804 clsk1indlem1 44504 r1rankcld 44690 fnchoice 45492 stoweidlem34 46491 stoweidlem59 46516 dirkercncflem2 46561 fourierdlem42 46606 iundjiunlem 46916 meaiininclem 46943 |
| Copyright terms: Public domain | W3C validator |