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

Syntax hints:   = wceq 1331   F/_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  7516  nfseq  10228  nfsum1  11125  nfsum  11126  nfcprod1  11323  nfcprod  11324