| 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 2730 | . 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶) | |
| 3 | 1, 2 | neleq12d 3034 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∉ wnel 3029 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-ext 2701 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2721 df-clel 2803 df-nel 3030 |
| This theorem is referenced by: ruALT 9498 ssnn0fi 13892 cnpart 15147 sqrmo 15158 resqrtcl 15160 resqrtthlem 15161 sqrtneg 15174 sqreu 15268 sqrtthlem 15270 eqsqrtd 15275 ge2nprmge4 16612 prmgaplem7 16969 mgmnsgrpex 18805 sgrpnmndex 18806 iccpnfcnv 24840 griedg0prc 29213 nbgrssovtx 29310 rgrusgrprc 29539 rusgrprc 29540 rgrprcx 29542 frgrwopreglem4a 30258 xrge0iifcnv 33916 0nn0m1nnn0 35106 fpprel 47732 gpg5nbgrvtx03star 48084 gpg5nbgr3star 48085 grlimedgnedg 48135 oddinmgm 48179 |
| Copyright terms: Public domain | W3C validator |