Theorem nfcri 2313

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

Syntax hints:   F/wnf 1460   e. wcel 2148   F/_wnfc 2306

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308

This theorem is referenced by:  clelsb1f  2323  nfnfc  2326  nfeq  2327  nfel  2328  cleqf  2344  sbabel  2346  r2alf  2494  r2exf  2495  nfrabxy  2657  cbvralfw  2694  cbvrexfw  2695  cbvralf  2696  cbvrexf  2697  cbvrab  2735  rmo3f  2934  nfccdeq  2960  sbcabel  3044  cbvcsbw  3061  cbvcsb  3062  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  dfss2f  3146  nfdif  3256  nfun  3291  nfin  3341  nfop  3794  nfiunxy  3912  nfiinxy  3913  nfiunya  3914  nfiinya  3915  cbviun  3923  cbviin  3924  iunxsngf  3964  cbvdisj  3990  nfdisjv  3992  disjiun  3998  nfmpt  4095  cbvmptf  4097  nffrfor  4348  onintrab2im  4517  tfis  4582  nfxp  4653  opeliunxp  4681  iunxpf  4775  elrnmpt1  4878  fvmptssdm  5600  nfmpo  5943  cbvmpox  5952  fmpox  6200  nffrec  6396  cc3  7266  nfsum1  11363  nfsum  11364  fsum2dlemstep  11441  fisumcom2  11445  nfcprod1  11561  nfcprod  11562  cbvprod  11565  fprod2dlemstep  11629  fprodcom2fi  11633  ctiunctlemudc  12437  ctiunctlemfo  12439