Theorem nfcri 2306

Description: Consequence of the not-free predicate. (Note that unlike nfcr 2304, 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 2305	. 2 |- ( y e. A -> A. x y e. A )
3	2	nfi 1455	1 |- F/ x y e. A

Syntax hints:   F/wnf 1453   e. wcel 2141   F/_wnfc 2299

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-cleq 2163  df-clel 2166  df-nfc 2301

This theorem is referenced by:  clelsb1f  2316  nfnfc  2319  nfeq  2320  nfel  2321  cleqf  2337  sbabel  2339  r2alf  2487  r2exf  2488  nfrabxy  2650  cbvralfw  2687  cbvrexfw  2688  cbvralf  2689  cbvrexf  2690  cbvrab  2728  rmo3f  2927  nfccdeq  2953  sbcabel  3036  cbvcsbw  3053  cbvcsb  3054  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  dfss2f  3138  nfdif  3248  nfun  3283  nfin  3333  nfop  3781  nfiunxy  3899  nfiinxy  3900  nfiunya  3901  nfiinya  3902  cbviun  3910  cbviin  3911  iunxsngf  3950  cbvdisj  3976  nfdisjv  3978  disjiun  3984  nfmpt  4081  cbvmptf  4083  nffrfor  4333  onintrab2im  4502  tfis  4567  nfxp  4638  opeliunxp  4666  iunxpf  4759  elrnmpt1  4862  fvmptssdm  5580  nfmpo  5922  cbvmpox  5931  fmpox  6179  nffrec  6375  cc3  7230  nfsum1  11319  nfsum  11320  fsum2dlemstep  11397  fisumcom2  11401  nfcprod1  11517  nfcprod  11518  cbvprod  11521  fprod2dlemstep  11585  fprodcom2fi  11589  ctiunctlemudc  12392  ctiunctlemfo  12394