Description: This is a copy of dfcleq in main. It is not sufficient to avoid reproving ax-8 as shown in in-ax8 . (Contributed by NM, 15-Sep-1993) (Revised by BJ, 24-Jun-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-dfcleq.basic | |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axextb | |- ( y = z <-> A. u ( u e. y <-> u e. z ) ) |
|
| 2 | axextb | |- ( t = t <-> A. v ( v e. t <-> v e. t ) ) |
|
| 3 | 1 2 | wl-df.cleq | |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) |