![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fneq2 | Unicode version |
Description: Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
fneq2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq2 2199 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | anbi2d 464 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-fn 5238 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-fn 5238 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3bitr4g 223 |
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 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-4 1521 ax-17 1537 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 df-fn 5238 |
This theorem is referenced by: fneq2d 5326 fneq2i 5330 feq2 5368 foeq2 5454 f1o00 5515 eqfnfv2 5635 tfr0dm 6347 tfrlemisucaccv 6350 tfrlemi1 6357 tfrlemi14d 6358 tfrexlem 6359 tfr1onlemsucfn 6365 tfr1onlemsucaccv 6366 tfr1onlembxssdm 6368 tfr1onlembfn 6369 tfr1onlemaccex 6373 tfr1onlemres 6374 ixpeq1 6735 0fz1 10075 |
Copyright terms: Public domain | W3C validator |