![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqneltrd | Structured version Visualization version GIF version |
Description: If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
eqneltrd.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
eqneltrd.2 | ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐶) |
Ref | Expression |
---|---|
eqneltrd | ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqneltrd.2 | . 2 ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐶) | |
2 | eqneltrd.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
3 | 2 | eleq1d 2819 | . 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) |
4 | 1, 3 | mtbird 325 | 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: eqneltrrd 2855 opabn1stprc 8039 omopth2 8580 fpwwe2 10634 znnn0nn 12669 sqrtneglem 15209 dvdsaddre2b 16246 2mulprm 16626 mreexmrid 17583 mplcoe1 21574 mplcoe5 21577 2sqn0 26917 fvnobday 27161 nn0xmulclb 31962 pmtrcnel 32228 cycpmco2lem5 32267 qsnzr 32532 extdg1id 32687 reprpmtf1o 33576 fmlafvel 34314 bj-snmooreb 35933 islln2a 38326 islpln2a 38357 islvol2aN 38401 oadif1lem 42062 oadif1 42063 oddfl 43922 sumnnodd 44281 sinaover2ne0 44519 dvnprodlem1 44597 dirker2re 44743 dirkerdenne0 44744 dirkertrigeqlem3 44751 dirkercncflem1 44754 dirkercncflem2 44755 dirkercncflem4 44757 fouriersw 44882 sqrtnegnre 45950 requad01 46224 |
Copyright terms: Public domain | W3C validator |