ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfcxfr Structured version   Unicode version

Theorem nfcxfr 2172
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nfceqi.1
nfcxfr.2  F/_
Assertion
Ref Expression
nfcxfr  F/_

Proof of Theorem nfcxfr
StepHypRef Expression
1 nfcxfr.2 . 2  F/_
2 nfceqi.1 . . 3
32nfceqi 2171 . 2  F/_  F/_
41, 3mpbir 134 1  F/_
Colors of variables: wff set class
Syntax hints:   wceq 1242   F/_wnfc 2162
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-cleq 2030  df-clel 2033  df-nfc 2164
This theorem is referenced by:  nfrab1  2483  nfrabxy  2484  nfdif  3059  nfun  3093  nfin  3137  nfpw  3363  nfpr  3411  nfsn  3421  nfop  3556  nfuni  3577  nfint  3616  nfiunxy  3674  nfiinxy  3675  nfiunya  3676  nfiinya  3677  nfiu1  3678  nfii1  3679  nfopab  3816  nfopab1  3817  nfopab2  3818  nfmpt  3840  nfmpt1  3841  repizf2  3906  nfsuc  4111  nfxp  4314  nfco  4444  nfcnv  4457  nfdm  4521  nfrn  4522  nfres  4557  nfima  4619  nfiota1  4812  nffv  5128  fvmptss2  5190  fvmptssdm  5198  fvmptf  5206  ralrnmpt  5252  rexrnmpt  5253  f1ompt  5263  f1mpt  5353  fliftfun  5379  nfriota1  5418  riotaprop  5434  nfoprab1  5496  nfoprab2  5497  nfoprab3  5498  nfoprab  5499  nfmpt21  5513  nfmpt22  5514  nfmpt2  5515  ovmpt2s  5566  ov2gf  5567  ovi3  5579  nftpos  5835  nfrecs  5863  nffrec  5921  xpcomco  6236  nfiseq  8898
  Copyright terms: Public domain W3C validator