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  2657  nfrabxy  2658  nfdif  3257  nfun  3292  nfin  3342  nfpw  3589  nfpr  3643  nfsn  3653  nfop  3795  nfuni  3816  nfint  3855  nfiunxy  3913  nfiinxy  3914  nfiunya  3915  nfiinya  3916  nfiu1  3917  nfii1  3918  nfopab  4072  nfopab1  4073  nfopab2  4074  nfmpt  4096  nfmpt1  4097  repizf2  4163  nfsuc  4409  nfxp  4654  nfco  4793  nfcnv  4807  nfdm  4872  nfrn  4873  nfres  4910  nfima  4979  nfiota1  5181  nffv  5526  fvmptss2  5592  fvmptssdm  5601  fvmptf  5609  ralrnmpt  5659  rexrnmpt  5660  f1ompt  5668  f1mpt  5772  fliftfun  5797  nfriota1  5838  riotaprop  5854  nfoprab1  5924  nfoprab2  5925  nfoprab3  5926  nfoprab  5927  nfmpo1  5942  nfmpo2  5943  nfmpo  5944  ovmpos  5998  ov2gf  5999  ovi3  6011  nfof  6088  nfofr  6089  nftpos  6280  nfrecs  6308  nffrec  6397  nfixpxy  6717  nfixp1  6718  xpcomco  6826  nfsup  6991  nfinf  7016  nfdju  7041  caucvgprprlemaddq  7707  nfseq  10455  nfsum1  11364  nfsum  11365  nfcprod1  11562  nfcprod  11563  lgseisenlem2  14454
  Copyright terms: Public domain W3C validator