![]() |
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 2772 | . 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶) | |
3 | 1, 2 | neleq12d 3050 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1631 ∉ wnel 3046 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ex 1853 df-cleq 2764 df-clel 2767 df-nel 3047 |
This theorem is referenced by: ruALT 8668 ssnn0fi 12992 cnpart 14188 sqrmo 14200 resqrtcl 14202 resqrtthlem 14203 sqrtneg 14216 sqreu 14308 sqrtthlem 14310 eqsqrtd 14315 prmgaplem7 15968 mgmnsgrpex 17626 sgrpnmndex 17627 iccpnfcnv 22963 griedg0prc 26379 nbgrssovtx 26480 nbgrssovtxOLD 26483 rgrusgrprc 26720 rusgrprc 26721 rgrprcx 26723 frgrwopreglem4a 27492 xrge0iifcnv 30319 oddinmgm 42340 |
Copyright terms: Public domain | W3C validator |