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  2658  cbvralfw  2695  cbvrexfw  2696  cbvralf  2697  cbvrexf  2698  cbvrab  2736  rmo3f  2935  nfccdeq  2961  sbcabel  3045  cbvcsbw  3062  cbvcsb  3063  cbvralcsf  3120  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  dfss2f  3147  nfdif  3257  nfun  3292  nfin  3342  nfop  3795  nfiunxy  3913  nfiinxy  3914  nfiunya  3915  nfiinya  3916  cbviun  3924  cbviin  3925  iunxsngf  3965  cbvdisj  3991  nfdisjv  3993  disjiun  3999  nfmpt  4096  cbvmptf  4098  nffrfor  4349  onintrab2im  4518  tfis  4583  nfxp  4654  opeliunxp  4682  iunxpf  4776  elrnmpt1  4879  fvmptssdm  5601  nfmpo  5944  cbvmpox  5953  fmpox  6201  nffrec  6397  cc3  7267  nfsum1  11364  nfsum  11365  fsum2dlemstep  11442  fisumcom2  11446  nfcprod1  11562  nfcprod  11563  cbvprod  11566  fprod2dlemstep  11630  fprodcom2fi  11634  ctiunctlemudc  12438  ctiunctlemfo  12440