![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfcxfr | Unicode version |
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfceqi.1 |
![]() ![]() ![]() ![]() |
nfcxfr.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfcxfr |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcxfr.2 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfceqi.1 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | nfceqi 2278 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpbir 145 |
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-5 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-17 1507 ax-ial 1515 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-cleq 2133 df-clel 2136 df-nfc 2271 |
This theorem is referenced by: nfrab1 2613 nfrabxy 2614 nfdif 3202 nfun 3237 nfin 3287 nfpw 3528 nfpr 3581 nfsn 3591 nfop 3729 nfuni 3750 nfint 3789 nfiunxy 3847 nfiinxy 3848 nfiunya 3849 nfiinya 3850 nfiu1 3851 nfii1 3852 nfopab 4004 nfopab1 4005 nfopab2 4006 nfmpt 4028 nfmpt1 4029 repizf2 4094 nfsuc 4338 nfxp 4574 nfco 4712 nfcnv 4726 nfdm 4791 nfrn 4792 nfres 4829 nfima 4897 nfiota1 5098 nffv 5439 fvmptss2 5504 fvmptssdm 5513 fvmptf 5521 ralrnmpt 5570 rexrnmpt 5571 f1ompt 5579 f1mpt 5680 fliftfun 5705 nfriota1 5745 riotaprop 5761 nfoprab1 5828 nfoprab2 5829 nfoprab3 5830 nfoprab 5831 nfmpo1 5846 nfmpo2 5847 nfmpo 5848 ovmpos 5902 ov2gf 5903 ovi3 5915 nfof 5995 nfofr 5996 nftpos 6184 nfrecs 6212 nffrec 6301 nfixpxy 6619 nfixp1 6620 xpcomco 6728 nfsup 6887 nfinf 6912 nfdju 6935 caucvgprprlemaddq 7540 nfseq 10259 nfsum1 11157 nfsum 11158 nfcprod1 11355 nfcprod 11356 |
Copyright terms: Public domain | W3C validator |