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 2308 | . 2 |
4 | 1, 3 | mpbir 145 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1348 wnfc 2299 |
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 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-cleq 2163 df-clel 2166 df-nfc 2301 |
This theorem is referenced by: nfrab1 2649 nfrabxy 2650 nfdif 3248 nfun 3283 nfin 3333 nfpw 3579 nfpr 3633 nfsn 3643 nfop 3781 nfuni 3802 nfint 3841 nfiunxy 3899 nfiinxy 3900 nfiunya 3901 nfiinya 3902 nfiu1 3903 nfii1 3904 nfopab 4057 nfopab1 4058 nfopab2 4059 nfmpt 4081 nfmpt1 4082 repizf2 4148 nfsuc 4393 nfxp 4638 nfco 4776 nfcnv 4790 nfdm 4855 nfrn 4856 nfres 4893 nfima 4961 nfiota1 5162 nffv 5506 fvmptss2 5571 fvmptssdm 5580 fvmptf 5588 ralrnmpt 5638 rexrnmpt 5639 f1ompt 5647 f1mpt 5750 fliftfun 5775 nfriota1 5816 riotaprop 5832 nfoprab1 5902 nfoprab2 5903 nfoprab3 5904 nfoprab 5905 nfmpo1 5920 nfmpo2 5921 nfmpo 5922 ovmpos 5976 ov2gf 5977 ovi3 5989 nfof 6066 nfofr 6067 nftpos 6258 nfrecs 6286 nffrec 6375 nfixpxy 6695 nfixp1 6696 xpcomco 6804 nfsup 6969 nfinf 6994 nfdju 7019 caucvgprprlemaddq 7670 nfseq 10411 nfsum1 11319 nfsum 11320 nfcprod1 11517 nfcprod 11518 |
Copyright terms: Public domain | W3C validator |