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 2817 | . 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) |
4 | 1, 3 | mtbird 328 | 1 ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1542 ∈ wcel 2113 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-cleq 2730 df-clel 2811 |
This theorem is referenced by: eqneltrrd 2853 opabn1stprc 7774 omopth2 8234 fpwwe2 10136 znnn0nn 12168 sqrtneglem 14709 dvdsaddre2b 15745 2mulprm 16127 mreexmrid 17010 mplcoe1 20841 mplcoe5 20844 2sqn0 26162 nn0xmulclb 30661 pmtrcnel 30927 cycpmco2lem5 30966 extdg1id 31302 reprpmtf1o 32168 fmlafvel 32910 fvnobday 33514 bj-snmooreb 34895 islln2a 37143 islpln2a 37174 islvol2aN 37218 oddfl 42337 sumnnodd 42697 sinaover2ne0 42935 dvnprodlem1 43013 dirker2re 43159 dirkerdenne0 43160 dirkertrigeqlem3 43167 dirkercncflem1 43170 dirkercncflem2 43171 dirkercncflem4 43173 fouriersw 43298 sqrtnegnre 44317 requad01 44591 |
Copyright terms: Public domain | W3C validator |