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 2822 | . 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶) | |
3 | 1, 2 | neleq12d 3127 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∉ wnel 3123 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-clel 2893 df-nel 3124 |
This theorem is referenced by: ruALT 9056 ssnn0fi 13343 cnpart 14589 sqrmo 14601 resqrtcl 14603 resqrtthlem 14604 sqrtneg 14617 sqreu 14710 sqrtthlem 14712 eqsqrtd 14717 ge2nprmge4 16035 prmgaplem7 16383 mgmnsgrpex 18036 sgrpnmndex 18037 iccpnfcnv 23477 griedg0prc 26974 nbgrssovtx 27071 rgrusgrprc 27299 rusgrprc 27300 rgrprcx 27302 frgrwopreglem4a 28017 xrge0iifcnv 31076 0nn0m1nnn0 32249 fpprel 43740 oddinmgm 43929 |
Copyright terms: Public domain | W3C validator |