Theorem nfcri 2302

Description: Consequence of the not-free predicate. (Note that unlike nfcr 2300, this does not require y and A to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfcri.1	|- F/_ x A

Assertion

Ref	Expression
nfcri	|- F/ x y e. A

Distinct variable group:   x, y

Allowed substitution hints:   A( x, y)

Proof of Theorem nfcri

Step	Hyp	Ref	Expression
1		nfcri.1	. . 3 |- F/_ x A
2	1	nfcrii 2301	. 2 |- ( y e. A -> A. x y e. A )
3	2	nfi 1450	1 |- F/ x y e. A

Syntax hints:   F/wnf 1448   e. wcel 2136   F/_wnfc 2295

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-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-cleq 2158  df-clel 2161  df-nfc 2297

This theorem is referenced by:  clelsb1f  2312  nfnfc  2315  nfeq  2316  nfel  2317  cleqf  2333  sbabel  2335  r2alf  2483  r2exf  2484  nfrabxy  2646  cbvralfw  2683  cbvrexfw  2684  cbvralf  2685  cbvrexf  2686  cbvrab  2724  rmo3f  2923  nfccdeq  2949  sbcabel  3032  cbvcsbw  3049  cbvcsb  3050  cbvralcsf  3107  cbvrexcsf  3108  cbvreucsf  3109  cbvrabcsf  3110  dfss2f  3133  nfdif  3243  nfun  3278  nfin  3328  nfop  3774  nfiunxy  3892  nfiinxy  3893  nfiunya  3894  nfiinya  3895  cbviun  3903  cbviin  3904  iunxsngf  3943  cbvdisj  3969  nfdisjv  3971  disjiun  3977  nfmpt  4074  cbvmptf  4076  nffrfor  4326  onintrab2im  4495  tfis  4560  nfxp  4631  opeliunxp  4659  iunxpf  4752  elrnmpt1  4855  fvmptssdm  5570  nfmpo  5911  cbvmpox  5920  fmpox  6168  nffrec  6364  cc3  7209  nfsum1  11297  nfsum  11298  fsum2dlemstep  11375  fisumcom2  11379  nfcprod1  11495  nfcprod  11496  cbvprod  11499  fprod2dlemstep  11563  fprodcom2fi  11567  ctiunctlemudc  12370  ctiunctlemfo  12372