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

Theorem nfcxfr 2278
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 2277 . 2 (𝑥𝐴𝑥𝐵)
41, 3mpbir 145 1 𝑥𝐴
Colors of variables: wff set class
Syntax hints:   = wceq 1331  wnfc 2268
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-cleq 2132  df-clel 2135  df-nfc 2270
This theorem is referenced by:  nfrab1  2610  nfrabxy  2611  nfdif  3197  nfun  3232  nfin  3282  nfpw  3523  nfpr  3573  nfsn  3583  nfop  3721  nfuni  3742  nfint  3781  nfiunxy  3839  nfiinxy  3840  nfiunya  3841  nfiinya  3842  nfiu1  3843  nfii1  3844  nfopab  3996  nfopab1  3997  nfopab2  3998  nfmpt  4020  nfmpt1  4021  repizf2  4086  nfsuc  4330  nfxp  4566  nfco  4704  nfcnv  4718  nfdm  4783  nfrn  4784  nfres  4821  nfima  4889  nfiota1  5090  nffv  5431  fvmptss2  5496  fvmptssdm  5505  fvmptf  5513  ralrnmpt  5562  rexrnmpt  5563  f1ompt  5571  f1mpt  5672  fliftfun  5697  nfriota1  5737  riotaprop  5753  nfoprab1  5820  nfoprab2  5821  nfoprab3  5822  nfoprab  5823  nfmpo1  5838  nfmpo2  5839  nfmpo  5840  ovmpos  5894  ov2gf  5895  ovi3  5907  nfof  5987  nfofr  5988  nftpos  6176  nfrecs  6204  nffrec  6293  nfixpxy  6611  nfixp1  6612  xpcomco  6720  nfsup  6879  nfinf  6904  nfdju  6927  caucvgprprlemaddq  7530  nfseq  10242  nfsum1  11139  nfsum  11140  nfcprod1  11337  nfcprod  11338
  Copyright terms: Public domain W3C validator