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 2295 | . 2 |
4 | 1, 3 | mpbir 145 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1335 wnfc 2286 |
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 1427 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-4 1490 ax-17 1506 ax-ial 1514 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-nf 1441 df-cleq 2150 df-clel 2153 df-nfc 2288 |
This theorem is referenced by: nfrab1 2636 nfrabxy 2637 nfdif 3228 nfun 3263 nfin 3313 nfpw 3556 nfpr 3609 nfsn 3619 nfop 3757 nfuni 3778 nfint 3817 nfiunxy 3875 nfiinxy 3876 nfiunya 3877 nfiinya 3878 nfiu1 3879 nfii1 3880 nfopab 4032 nfopab1 4033 nfopab2 4034 nfmpt 4056 nfmpt1 4057 repizf2 4123 nfsuc 4368 nfxp 4613 nfco 4751 nfcnv 4765 nfdm 4830 nfrn 4831 nfres 4868 nfima 4936 nfiota1 5137 nffv 5478 fvmptss2 5543 fvmptssdm 5552 fvmptf 5560 ralrnmpt 5609 rexrnmpt 5610 f1ompt 5618 f1mpt 5721 fliftfun 5746 nfriota1 5787 riotaprop 5803 nfoprab1 5870 nfoprab2 5871 nfoprab3 5872 nfoprab 5873 nfmpo1 5888 nfmpo2 5889 nfmpo 5890 ovmpos 5944 ov2gf 5945 ovi3 5957 nfof 6037 nfofr 6038 nftpos 6226 nfrecs 6254 nffrec 6343 nfixpxy 6662 nfixp1 6663 xpcomco 6771 nfsup 6936 nfinf 6961 nfdju 6986 caucvgprprlemaddq 7628 nfseq 10354 nfsum1 11253 nfsum 11254 nfcprod1 11451 nfcprod 11452 |
Copyright terms: Public domain | W3C validator |