Theorem nfcxfr 2369

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 2368	. 2 |- ( F/_ x A <-> F/_ x B )
4	1, 3	mpbir 146	1 |- F/_ x A

Syntax hints:   = wceq 1395   F/_wnfc 2359

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-cleq 2222  df-clel 2225  df-nfc 2361

This theorem is referenced by:  nfrab1  2711  nfrabw  2712  nfdif  3325  nfun  3360  nfin  3410  nfpw  3662  nfpr  3716  nfsn  3726  nfop  3873  nfuni  3894  nfint  3933  nfiunxy  3991  nfiinxy  3992  nfiunya  3993  nfiinya  3994  nfiu1  3995  nfii1  3996  nfopab  4152  nfopab1  4153  nfopab2  4154  nfmpt  4176  nfmpt1  4177  repizf2  4246  nfsuc  4499  nfxp  4746  nfco  4887  nfcnv  4901  nfdm  4968  nfrn  4969  nfres  5007  nfima  5076  nfiota1  5280  nffv  5639  fvmptss2  5711  fvmptssdm  5721  fvmptf  5729  ralrnmpt  5779  rexrnmpt  5780  f1ompt  5788  f1mpt  5901  fliftfun  5926  nfriota1  5968  riotaprop  5986  nfoprab1  6059  nfoprab2  6060  nfoprab3  6061  nfoprab  6062  nfmpo1  6077  nfmpo2  6078  nfmpo  6079  ovmpos  6134  ov2gf  6135  ovi3  6148  nfof  6230  nfofr  6231  nftpos  6431  nfrecs  6459  nffrec  6548  nfixpxy  6872  nfixp1  6873  xpcomco  6993  nfsup  7167  nfinf  7192  nfdju  7217  caucvgprprlemaddq  7903  nfseq  10687  nfwrd  11108  nfsum1  11875  nfsum  11876  nfcprod1  12073  nfcprod  12074  lgseisenlem2  15758  lfgrnloopen  15939