![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > neleq1 | Structured version Visualization version GIF version |
Description: Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.) |
Ref | Expression |
---|---|
neleq1 | ⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) | |
2 | eqidd 2727 | . 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶) | |
3 | 1, 2 | neleq12d 3041 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 ∉ wnel 3036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-clel 2803 df-nel 3037 |
This theorem is referenced by: ruALT 9646 ssnn0fi 14005 cnpart 15245 sqrmo 15256 resqrtcl 15258 resqrtthlem 15259 sqrtneg 15272 sqreu 15365 sqrtthlem 15367 eqsqrtd 15372 ge2nprmge4 16702 prmgaplem7 17059 mgmnsgrpex 18921 sgrpnmndex 18922 iccpnfcnv 24960 griedg0prc 29200 nbgrssovtx 29297 rgrusgrprc 29526 rusgrprc 29527 rgrprcx 29529 frgrwopreglem4a 30243 xrge0iifcnv 33748 0nn0m1nnn0 34940 fpprel 47300 oddinmgm 47552 |
Copyright terms: Public domain | W3C validator |