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

Theorem nfcxfr 2225
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 𝑥𝐵
Assertion
Ref Expression
nfcxfr 𝑥𝐴

Proof of Theorem nfcxfr
StepHypRef Expression
1 nfcxfr.2 . 2 𝑥𝐵
2 nfceqi.1 . . 3 𝐴 = 𝐵
32nfceqi 2224 . 2 (𝑥𝐴𝑥𝐵)
41, 3mpbir 144 1 𝑥𝐴
Colors of variables: wff set class
Syntax hints:   = wceq 1289  wnfc 2215
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-cleq 2081  df-clel 2084  df-nfc 2217
This theorem is referenced by:  nfrab1  2546  nfrabxy  2547  nfdif  3119  nfun  3154  nfin  3204  nfpw  3437  nfpr  3487  nfsn  3497  nfop  3633  nfuni  3654  nfint  3693  nfiunxy  3751  nfiinxy  3752  nfiunya  3753  nfiinya  3754  nfiu1  3755  nfii1  3756  nfopab  3898  nfopab1  3899  nfopab2  3900  nfmpt  3922  nfmpt1  3923  repizf2  3989  nfsuc  4226  nfxp  4454  nfco  4589  nfcnv  4603  nfdm  4667  nfrn  4668  nfres  4703  nfima  4769  nfiota1  4969  nffv  5299  fvmptss2  5363  fvmptssdm  5371  fvmptf  5379  ralrnmpt  5425  rexrnmpt  5426  f1ompt  5434  f1mpt  5532  fliftfun  5557  nfriota1  5597  riotaprop  5613  nfoprab1  5680  nfoprab2  5681  nfoprab3  5682  nfoprab  5683  nfmpt21  5697  nfmpt22  5698  nfmpt2  5699  ovmpt2s  5750  ov2gf  5751  ovi3  5763  nfof  5843  nfofr  5844  nftpos  6026  nfrecs  6054  nffrec  6143  xpcomco  6522  nfsup  6666  nfinf  6691  nfdju  6714  caucvgprprlemaddq  7246  nfiseq  9833  nfseq  9834  nfsum1  10709  nfsum  10710
  Copyright terms: Public domain W3C validator