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

Theorem nfcxfr 2255
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 2254 . 2 (𝑥𝐴𝑥𝐵)
41, 3mpbir 145 1 𝑥𝐴
Colors of variables: wff set class
Syntax hints:   = wceq 1316  wnfc 2245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-cleq 2110  df-clel 2113  df-nfc 2247
This theorem is referenced by:  nfrab1  2587  nfrabxy  2588  nfdif  3167  nfun  3202  nfin  3252  nfpw  3493  nfpr  3543  nfsn  3553  nfop  3691  nfuni  3712  nfint  3751  nfiunxy  3809  nfiinxy  3810  nfiunya  3811  nfiinya  3812  nfiu1  3813  nfii1  3814  nfopab  3966  nfopab1  3967  nfopab2  3968  nfmpt  3990  nfmpt1  3991  repizf2  4056  nfsuc  4300  nfxp  4536  nfco  4674  nfcnv  4688  nfdm  4753  nfrn  4754  nfres  4791  nfima  4859  nfiota1  5060  nffv  5399  fvmptss2  5464  fvmptssdm  5473  fvmptf  5481  ralrnmpt  5530  rexrnmpt  5531  f1ompt  5539  f1mpt  5640  fliftfun  5665  nfriota1  5705  riotaprop  5721  nfoprab1  5788  nfoprab2  5789  nfoprab3  5790  nfoprab  5791  nfmpo1  5806  nfmpo2  5807  nfmpo  5808  ovmpos  5862  ov2gf  5863  ovi3  5875  nfof  5955  nfofr  5956  nftpos  6144  nfrecs  6172  nffrec  6261  nfixpxy  6579  nfixp1  6580  xpcomco  6688  nfsup  6847  nfinf  6872  nfdju  6895  caucvgprprlemaddq  7484  nfseq  10196  nfsum1  11093  nfsum  11094
  Copyright terms: Public domain W3C validator