Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfeq | Unicode version |
Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfnfc.1 | |
nfeq.2 |
Ref | Expression |
---|---|
nfeq |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfcleq 2034 | . 2 | |
2 | nfnfc.1 | . . . . 5 | |
3 | 2 | nfcri 2172 | . . . 4 |
4 | nfeq.2 | . . . . 5 | |
5 | 4 | nfcri 2172 | . . . 4 |
6 | 3, 5 | nfbi 1481 | . . 3 |
7 | 6 | nfal 1468 | . 2 |
8 | 1, 7 | nfxfr 1363 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 98 wal 1241 wceq 1243 wnf 1349 wcel 1393 wnfc 2165 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-nf 1350 df-sb 1646 df-cleq 2033 df-clel 2036 df-nfc 2167 |
This theorem is referenced by: nfel 2186 nfeq1 2187 nfeq2 2189 nfne 2297 raleqf 2501 rexeqf 2502 reueq1f 2503 rmoeq1f 2504 rabeqf 2550 sbceqg 2866 csbhypf 2885 nfiotadxy 4870 nffn 4995 nffo 5105 fvmptdf 5258 mpteqb 5261 fvmptf 5263 eqfnfv2f 5269 dff13f 5409 ovmpt2s 5624 ov2gf 5625 ovmpt2dxf 5626 ovmpt2df 5632 eqerlem 6137 |
Copyright terms: Public domain | W3C validator |