![]() |
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 2798 | . 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶) | |
3 | 1, 2 | neleq12d 3096 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1525 ∉ wnel 3092 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1766 df-cleq 2790 df-clel 2865 df-nel 3093 |
This theorem is referenced by: ruALT 8920 ssnn0fi 13207 cnpart 14437 sqrmo 14449 resqrtcl 14451 resqrtthlem 14452 sqrtneg 14465 sqreu 14558 sqrtthlem 14560 eqsqrtd 14565 ge2nprmge4 15878 prmgaplem7 16226 mgmnsgrpex 17861 sgrpnmndex 17862 iccpnfcnv 23235 griedg0prc 26733 nbgrssovtx 26830 rgrusgrprc 27058 rusgrprc 27059 rgrprcx 27061 frgrwopreglem4a 27777 xrge0iifcnv 30789 0nn0m1nnn0 31961 fpprel 43397 oddinmgm 43586 |
Copyright terms: Public domain | W3C validator |