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  3793  nfiunxy  3911  nfiinxy  3912  nfiunya  3913  nfiinya  3914  cbviun  3922  cbviin  3923  iunxsngf  3962  cbvdisj  3988  nfdisjv  3990  disjiun  3996  nfmpt  4093  cbvmptf  4095  nffrfor  4346  onintrab2im  4515  tfis  4580  nfxp  4651  opeliunxp  4679  iunxpf  4772  elrnmpt1  4875  fvmptssdm  5597  nfmpo  5939  cbvmpox  5948  fmpox  6196  nffrec  6392  cc3  7262  nfsum1  11355  nfsum  11356  fsum2dlemstep  11433  fisumcom2  11437  nfcprod1  11553  nfcprod  11554  cbvprod  11557  fprod2dlemstep  11621  fprodcom2fi  11625  ctiunctlemudc  12428  ctiunctlemfo  12430