Theorem nfcri 2344

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

Syntax hints:   F/wnf 1484   e. wcel 2178   F/_wnfc 2337

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-cleq 2200  df-clel 2203  df-nfc 2339

This theorem is referenced by:  clelsb1f  2354  nfnfc  2357  nfeq  2358  nfel  2359  cleqf  2375  sbabel  2377  r2alf  2525  r2exf  2526  nfrabw  2689  cbvralfw  2731  cbvrexfw  2732  cbvralf  2733  cbvrexf  2734  cbvrab  2774  rmo3f  2977  nfccdeq  3003  sbcabel  3088  cbvcsbw  3105  cbvcsb  3106  cbvralcsf  3164  cbvrexcsf  3165  cbvreucsf  3166  cbvrabcsf  3167  dfss2f  3192  nfdif  3302  nfun  3337  nfin  3387  nfop  3849  nfiunxy  3967  nfiinxy  3968  nfiunya  3969  nfiinya  3970  cbviun  3978  cbviin  3979  iunxsngf  4019  cbvdisj  4045  nfdisjv  4047  disjiun  4054  nfmpt  4152  cbvmptf  4154  nffrfor  4413  onintrab2im  4584  tfis  4649  nfxp  4720  opeliunxp  4748  iunxpf  4844  elrnmpt1  4948  fvmptssdm  5687  nfmpo  6037  cbvmpox  6046  fmpox  6309  nffrec  6505  cc3  7415  nfsum1  11782  nfsum  11783  fsum2dlemstep  11860  fisumcom2  11864  nfcprod1  11980  nfcprod  11981  cbvprod  11984  fprod2dlemstep  12048  fprodcom2fi  12052  ctiunctlemudc  12923  ctiunctlemfo  12925