Theorem nfcxfr 2276

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	|- A = B
nfcxfr.2	|- F/_ x B

Assertion

Ref	Expression
nfcxfr	|- F/_ x A

Proof of Theorem nfcxfr

Step	Hyp	Ref	Expression
1		nfcxfr.2	. 2 |- F/_ x B
2		nfceqi.1	. . 3 |- A = B
3	2	nfceqi 2275	. 2 |- ( F/_ x A <-> F/_ x B )
4	1, 3	mpbir 145	1 |- F/_ x A

Syntax hints:   = wceq 1331   F/_wnfc 2266

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 2119

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-cleq 2130  df-clel 2133  df-nfc 2268

This theorem is referenced by:  nfrab1  2608  nfrabxy  2609  nfdif  3192  nfun  3227  nfin  3277  nfpw  3518  nfpr  3568  nfsn  3578  nfop  3716  nfuni  3737  nfint  3776  nfiunxy  3834  nfiinxy  3835  nfiunya  3836  nfiinya  3837  nfiu1  3838  nfii1  3839  nfopab  3991  nfopab1  3992  nfopab2  3993  nfmpt  4015  nfmpt1  4016  repizf2  4081  nfsuc  4325  nfxp  4561  nfco  4699  nfcnv  4713  nfdm  4778  nfrn  4779  nfres  4816  nfima  4884  nfiota1  5085  nffv  5424  fvmptss2  5489  fvmptssdm  5498  fvmptf  5506  ralrnmpt  5555  rexrnmpt  5556  f1ompt  5564  f1mpt  5665  fliftfun  5690  nfriota1  5730  riotaprop  5746  nfoprab1  5813  nfoprab2  5814  nfoprab3  5815  nfoprab  5816  nfmpo1  5831  nfmpo2  5832  nfmpo  5833  ovmpos  5887  ov2gf  5888  ovi3  5900  nfof  5980  nfofr  5981  nftpos  6169  nfrecs  6197  nffrec  6286  nfixpxy  6604  nfixp1  6605  xpcomco  6713  nfsup  6872  nfinf  6897  nfdju  6920  caucvgprprlemaddq  7509  nfseq  10221  nfsum1  11118  nfsum  11119  nfcprod1  11316  nfcprod  11317