|   | 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 2742 | . 2 ⊢ (𝜑 → 𝐵 = 𝐴) | 
| 4 | 1, 3 | neleqtrd 2862 | 1 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1539 ∈ wcel 2107 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-cleq 2728 df-clel 2815 | 
| This theorem is referenced by: csbxp 5784 omopth2 8623 wrdlndm 14569 mreexd 17686 mreexmrid 17687 psgnunilem2 19514 lspindp4 21140 lsppratlem3 21152 frlmlbs 21818 mdetralt 22615 lebnumlem1 24994 mideulem2 28743 opphllem 28744 structiedg0val 29040 snstriedgval 29056 1hevtxdg0 29524 cyc2fvx 33155 cyc3co2 33161 elrgspnlem4 33250 lindssn 33407 qqhval2lem 33983 qqhf 33988 unbdqndv1 36510 lindsenlbs 37623 mapdindp2 41724 mapdindp4 41726 mapdh6dN 41742 hdmap1l6d 41816 tfsconcatb0 43362 clsk1indlem1 44063 r1rankcld 44255 fnchoice 45039 stoweidlem34 46054 stoweidlem59 46079 dirkercncflem2 46124 fourierdlem42 46169 iundjiunlem 46479 meaiininclem 46506 | 
| Copyright terms: Public domain | W3C validator |