![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfcxfr | GIF 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 2315 | . 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵) |
4 | 1, 3 | mpbir 146 | 1 ⊢ Ⅎ𝑥𝐴 |
Colors of variables: wff set class |
Syntax hints: = wceq 1353 Ⅎwnfc 2306 |
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 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-cleq 2170 df-clel 2173 df-nfc 2308 |
This theorem is referenced by: nfrab1 2656 nfrabxy 2657 nfdif 3256 nfun 3291 nfin 3341 nfpw 3587 nfpr 3641 nfsn 3651 nfop 3792 nfuni 3813 nfint 3852 nfiunxy 3910 nfiinxy 3911 nfiunya 3912 nfiinya 3913 nfiu1 3914 nfii1 3915 nfopab 4068 nfopab1 4069 nfopab2 4070 nfmpt 4092 nfmpt1 4093 repizf2 4159 nfsuc 4404 nfxp 4649 nfco 4787 nfcnv 4801 nfdm 4866 nfrn 4867 nfres 4904 nfima 4973 nfiota1 5175 nffv 5520 fvmptss2 5586 fvmptssdm 5595 fvmptf 5603 ralrnmpt 5653 rexrnmpt 5654 f1ompt 5662 f1mpt 5765 fliftfun 5790 nfriota1 5831 riotaprop 5847 nfoprab1 5917 nfoprab2 5918 nfoprab3 5919 nfoprab 5920 nfmpo1 5935 nfmpo2 5936 nfmpo 5937 ovmpos 5991 ov2gf 5992 ovi3 6004 nfof 6081 nfofr 6082 nftpos 6273 nfrecs 6301 nffrec 6390 nfixpxy 6710 nfixp1 6711 xpcomco 6819 nfsup 6984 nfinf 7009 nfdju 7034 caucvgprprlemaddq 7685 nfseq 10428 nfsum1 11335 nfsum 11336 nfcprod1 11533 nfcprod 11534 |
Copyright terms: Public domain | W3C validator |