Theorem nfcxfr 2336

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

Syntax hints:   = wceq 1364   F/_wnfc 2326

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-cleq 2189  df-clel 2192  df-nfc 2328

This theorem is referenced by:  nfrab1  2677  nfrabw  2678  nfdif  3284  nfun  3319  nfin  3369  nfpw  3618  nfpr  3672  nfsn  3682  nfop  3824  nfuni  3845  nfint  3884  nfiunxy  3942  nfiinxy  3943  nfiunya  3944  nfiinya  3945  nfiu1  3946  nfii1  3947  nfopab  4101  nfopab1  4102  nfopab2  4103  nfmpt  4125  nfmpt1  4126  repizf2  4195  nfsuc  4443  nfxp  4690  nfco  4831  nfcnv  4845  nfdm  4910  nfrn  4911  nfres  4948  nfima  5017  nfiota1  5221  nffv  5568  fvmptss2  5636  fvmptssdm  5646  fvmptf  5654  ralrnmpt  5704  rexrnmpt  5705  f1ompt  5713  f1mpt  5818  fliftfun  5843  nfriota1  5885  riotaprop  5901  nfoprab1  5971  nfoprab2  5972  nfoprab3  5973  nfoprab  5974  nfmpo1  5989  nfmpo2  5990  nfmpo  5991  ovmpos  6046  ov2gf  6047  ovi3  6060  nfof  6141  nfofr  6142  nftpos  6337  nfrecs  6365  nffrec  6454  nfixpxy  6776  nfixp1  6777  xpcomco  6885  nfsup  7058  nfinf  7083  nfdju  7108  caucvgprprlemaddq  7775  nfseq  10549  nfwrd  10963  nfsum1  11521  nfsum  11522  nfcprod1  11719  nfcprod  11720  lgseisenlem2  15312