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

Theorem nfcxfr 2316
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 2315 . 2 (𝑥𝐴𝑥𝐵)
41, 3mpbir 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