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 2611 | . 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶) | |
3 | 1, 2 | neleq12d 2887 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 ∉ wnel 2781 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-cleq 2603 df-clel 2606 df-nel 2783 |
This theorem is referenced by: ruALT 8391 ssnn0fi 12646 cnpart 13828 sqrmo 13840 resqrtcl 13842 resqrtthlem 13843 sqrtneg 13856 sqreu 13948 sqrtthlem 13950 eqsqrtd 13955 prmgaplem7 15599 mgmnsgrpex 17241 sgrpnmndex 17242 iccpnfcnv 22551 frgrawopreglem4 26574 xrge0iifcnv 29307 griedg0prc 40488 nbgrssovtx 40586 rgrusgrprc 40789 rusgrprc 40790 rgrprcx 40792 frgrwopreglem4 41484 oddinmgm 41605 |
Copyright terms: Public domain | W3C validator |