Theorem nfcri 2326

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

Syntax hints:   F/wnf 1471   e. wcel 2160   F/_wnfc 2319

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-cleq 2182  df-clel 2185  df-nfc 2321

This theorem is referenced by:  clelsb1f  2336  nfnfc  2339  nfeq  2340  nfel  2341  cleqf  2357  sbabel  2359  r2alf  2507  r2exf  2508  nfrabxy  2671  cbvralfw  2708  cbvrexfw  2709  cbvralf  2710  cbvrexf  2711  cbvrab  2750  rmo3f  2949  nfccdeq  2975  sbcabel  3059  cbvcsbw  3076  cbvcsb  3077  cbvralcsf  3134  cbvrexcsf  3135  cbvreucsf  3136  cbvrabcsf  3137  dfss2f  3161  nfdif  3271  nfun  3306  nfin  3356  nfop  3809  nfiunxy  3927  nfiinxy  3928  nfiunya  3929  nfiinya  3930  cbviun  3938  cbviin  3939  iunxsngf  3979  cbvdisj  4005  nfdisjv  4007  disjiun  4013  nfmpt  4110  cbvmptf  4112  nffrfor  4366  onintrab2im  4535  tfis  4600  nfxp  4671  opeliunxp  4699  iunxpf  4793  elrnmpt1  4896  fvmptssdm  5621  nfmpo  5965  cbvmpox  5974  fmpox  6225  nffrec  6421  cc3  7297  nfsum1  11396  nfsum  11397  fsum2dlemstep  11474  fisumcom2  11478  nfcprod1  11594  nfcprod  11595  cbvprod  11598  fprod2dlemstep  11662  fprodcom2fi  11666  ctiunctlemudc  12488  ctiunctlemfo  12490