Description: Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994) (Proof shortened by Wolf Lammen, 25-Nov-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | neleq1 | |- ( A = B -> ( A e/ C <-> B e/ C ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | |- ( A = B -> A = B ) |
|
2 | eqidd | |- ( A = B -> C = C ) |
|
3 | 1 2 | neleq12d | |- ( A = B -> ( A e/ C <-> B e/ C ) ) |