![]() |
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 2739 | . 2 ⊢ (𝜑 → 𝐵 = 𝐴) |
4 | 1, 3 | neleqtrd 2856 | 1 ⊢ (𝜑 → ¬ 𝐶 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1542 ∈ wcel 2107 |
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-ex 1783 df-cleq 2725 df-clel 2811 |
This theorem is referenced by: csbxp 5732 omopth2 8532 wrdlndm 14424 mreexd 17527 mreexmrid 17528 psgnunilem2 19282 lspindp4 20614 lsppratlem3 20626 frlmlbs 21219 mdetralt 21973 lebnumlem1 24340 mideulem2 27718 opphllem 27719 structiedg0val 28015 snstriedgval 28031 1hevtxdg0 28495 cyc2fvx 32032 cyc3co2 32038 lindssn 32213 qqhval2lem 32619 qqhf 32624 unbdqndv1 35017 lindsenlbs 36119 mapdindp2 40230 mapdindp4 40232 mapdh6dN 40248 hdmap1l6d 40322 clsk1indlem1 42405 r1rankcld 42599 fnchoice 43322 stoweidlem34 44361 stoweidlem59 44386 dirkercncflem2 44431 fourierdlem42 44476 iundjiunlem 44786 meaiininclem 44813 |
Copyright terms: Public domain | W3C validator |