Theorem nfcri 2342

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

Syntax hints:   F/wnf 1483   e. wcel 2176   F/_wnfc 2335

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-cleq 2198  df-clel 2201  df-nfc 2337

This theorem is referenced by:  clelsb1f  2352  nfnfc  2355  nfeq  2356  nfel  2357  cleqf  2373  sbabel  2375  r2alf  2523  r2exf  2524  nfrabw  2687  cbvralfw  2728  cbvrexfw  2729  cbvralf  2730  cbvrexf  2731  cbvrab  2770  rmo3f  2970  nfccdeq  2996  sbcabel  3080  cbvcsbw  3097  cbvcsb  3098  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  dfss2f  3184  nfdif  3294  nfun  3329  nfin  3379  nfop  3835  nfiunxy  3953  nfiinxy  3954  nfiunya  3955  nfiinya  3956  cbviun  3964  cbviin  3965  iunxsngf  4005  cbvdisj  4031  nfdisjv  4033  disjiun  4039  nfmpt  4136  cbvmptf  4138  nffrfor  4395  onintrab2im  4566  tfis  4631  nfxp  4702  opeliunxp  4730  iunxpf  4826  elrnmpt1  4929  fvmptssdm  5664  nfmpo  6014  cbvmpox  6023  fmpox  6286  nffrec  6482  cc3  7380  nfsum1  11667  nfsum  11668  fsum2dlemstep  11745  fisumcom2  11749  nfcprod1  11865  nfcprod  11866  cbvprod  11869  fprod2dlemstep  11933  fprodcom2fi  11937  ctiunctlemudc  12808  ctiunctlemfo  12810