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  3779  nfiunxy  3897  nfiinxy  3898  nfiunya  3899  nfiinya  3900  cbviun  3908  cbviin  3909  iunxsngf  3948  cbvdisj  3974  nfdisjv  3976  disjiun  3982  nfmpt  4079  cbvmptf  4081  nffrfor  4331  onintrab2im  4500  tfis  4565  nfxp  4636  opeliunxp  4664  iunxpf  4757  elrnmpt1  4860  fvmptssdm  5578  nfmpo  5919  cbvmpox  5928  fmpox  6176  nffrec  6372  cc3  7217  nfsum1  11306  nfsum  11307  fsum2dlemstep  11384  fisumcom2  11388  nfcprod1  11504  nfcprod  11505  cbvprod  11508  fprod2dlemstep  11572  fprodcom2fi  11576  ctiunctlemudc  12379  ctiunctlemfo  12381