Theorem nfcxfr 2216

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

Syntax hints:   = wceq 1284   F/_wnfc 2206

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-cleq 2074  df-clel 2077  df-nfc 2208

This theorem is referenced by:  nfrab1  2533  nfrabxy  2534  nfdif  3093  nfun  3128  nfin  3172  nfpw  3394  nfpr  3442  nfsn  3452  nfop  3586  nfuni  3607  nfint  3646  nfiunxy  3704  nfiinxy  3705  nfiunya  3706  nfiinya  3707  nfiu1  3708  nfii1  3709  nfopab  3846  nfopab1  3847  nfopab2  3848  nfmpt  3870  nfmpt1  3871  repizf2  3936  nfsuc  4163  nfxp  4389  nfco  4519  nfcnv  4532  nfdm  4596  nfrn  4597  nfres  4632  nfima  4696  nfiota1  4889  nffv  5205  fvmptss2  5268  fvmptssdm  5276  fvmptf  5284  ralrnmpt  5330  rexrnmpt  5331  f1ompt  5341  f1mpt  5431  fliftfun  5456  nfriota1  5495  riotaprop  5511  nfoprab1  5574  nfoprab2  5575  nfoprab3  5576  nfoprab  5577  nfmpt21  5591  nfmpt22  5592  nfmpt2  5593  ovmpt2s  5644  ov2gf  5645  ovi3  5657  nftpos  5917  nfrecs  5945  nffrec  6005  xpcomco  6323  nfsup  6405  nfinf  6430  caucvgprprlemaddq  6898  nfiseq  9438  nfsum1  10193  nfsum  10194