![]() |
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 2134 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | nfnfc.1 |
. . . . 5
![]() ![]() ![]() ![]() | |
3 | 2 | nfcri 2276 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() |
4 | nfeq.2 |
. . . . 5
![]() ![]() ![]() ![]() | |
5 | 4 | nfcri 2276 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | nfbi 1569 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | nfal 1556 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 7 | nfxfr 1451 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-cleq 2133 df-clel 2136 df-nfc 2271 |
This theorem is referenced by: nfel 2291 nfeq1 2292 nfeq2 2294 nfne 2402 raleqf 2625 rexeqf 2626 reueq1f 2627 rmoeq1f 2628 rabeqf 2679 sbceqg 3023 csbhypf 3043 nfiotadw 5099 nffn 5227 nffo 5352 fvmptdf 5516 mpteqb 5519 fvmptf 5521 eqfnfv2f 5530 dff13f 5679 ovmpos 5902 ov2gf 5903 ovmpodxf 5904 ovmpodf 5910 eqerlem 6468 sumeq2 11160 fsumadd 11207 prodeq1f 11353 prodeq2 11358 txcnp 12479 cnmpt11 12491 cnmpt21 12499 cnmptcom 12506 |
Copyright terms: Public domain | W3C validator |