Definition df-ne 1192

Description: Define inequality.

Assertion

Ref	Expression
df-ne	|- (A =/= B <-> -. A = B)

Detailed syntax breakdown of Definition df-ne

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	wne 1190	. 2 wff A =/= B
4	1, 2	wceq 1091	. . 3 wff A = B
5	4	wn 1	. 2 wff -. A = B
6	3, 5	wb 127	1 wff (A =/= B <-> -. A = B)

This definition is referenced by:  neeq1 1194  neeq2 1195  necom 1198  dfpss2 1557  ax1ne0 4075  axrecex 4079  axrrecex 4081  axsup 4088  mul0or 4210  muln0bt 4213  divval 4217  divneq0bt 4230  gt0ne0 4340  lt01 4377  eqneg 4378  negne0 4379  recgt0i 4385  nnne0t 4444  sup3 4511  nnunb 4520  ine0 4524  irec 4526  crulem 4528  halfnz 4586  sqznn 4600  uzwo 4605  nnwoOLD 4608  nnwos 4610  uzwo3lem1 4614  sqegt0 4703  discrlem3 4715  sqrlem6 4736  cjre 4811  abslem2i 4866  axhis42 5049  bcs 5101  h1de2b 5459  h1de2ctlem 5460  spansneleq 5475  h1datom 5483  strlem1 5691  large 5700

metamath.org