Theorem nfcri 2368

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

Syntax hints:   F/wnf 1508   e. wcel 2202   F/_wnfc 2361

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-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2363

This theorem is referenced by:  clelsb1f  2378  nfnfc  2381  nfeq  2382  nfel  2383  cleqf  2399  sbabel  2401  r2alf  2549  r2exf  2550  nfrabw  2714  cbvralfw  2756  cbvrexfw  2757  cbvralf  2758  cbvrexf  2759  cbvrab  2800  rmo3f  3003  nfccdeq  3029  sbcabel  3114  cbvcsbw  3131  cbvcsb  3132  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  dfss2f  3218  nfdif  3328  nfun  3363  nfin  3413  nfop  3878  nfiunxy  3996  nfiinxy  3997  nfiunya  3998  nfiinya  3999  cbviun  4007  cbviin  4008  iunxsngf  4048  cbvdisj  4074  nfdisjv  4076  disjiun  4083  nfmpt  4181  cbvmptf  4183  nffrfor  4445  onintrab2im  4616  tfis  4681  nfxp  4752  opeliunxp  4781  iunxpf  4878  elrnmpt1  4983  fvmptssdm  5731  nfmpo  6089  cbvmpox  6098  fmpox  6364  nffrec  6561  cc3  7486  nfsum1  11916  nfsum  11917  fsum2dlemstep  11994  fisumcom2  11998  nfcprod1  12114  nfcprod  12115  cbvprod  12118  fprod2dlemstep  12182  fprodcom2fi  12186  ctiunctlemudc  13057  ctiunctlemfo  13059