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 2823 | . 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) |
4 | 1, 3 | mtbird 325 | 1 ⊢ (𝜑 → ¬ 𝐴 ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1539 ∈ wcel 2106 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-cleq 2730 df-clel 2816 |
This theorem is referenced by: eqneltrrd 2859 opabn1stprc 7898 omopth2 8415 fpwwe2 10399 znnn0nn 12433 sqrtneglem 14978 dvdsaddre2b 16016 2mulprm 16398 mreexmrid 17352 mplcoe1 21238 mplcoe5 21241 2sqn0 26582 nn0xmulclb 31094 pmtrcnel 31358 cycpmco2lem5 31397 extdg1id 31738 reprpmtf1o 32606 fmlafvel 33347 fvnobday 33881 bj-snmooreb 35285 islln2a 37531 islpln2a 37562 islvol2aN 37606 oddfl 42816 sumnnodd 43171 sinaover2ne0 43409 dvnprodlem1 43487 dirker2re 43633 dirkerdenne0 43634 dirkertrigeqlem3 43641 dirkercncflem1 43644 dirkercncflem2 43645 dirkercncflem4 43647 fouriersw 43772 sqrtnegnre 44799 requad01 45073 |
Copyright terms: Public domain | W3C validator |