Theorem nfcri 2333

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

Syntax hints:   F/wnf 1474   e. wcel 2167   F/_wnfc 2326

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-cleq 2189  df-clel 2192  df-nfc 2328

This theorem is referenced by:  clelsb1f  2343  nfnfc  2346  nfeq  2347  nfel  2348  cleqf  2364  sbabel  2366  r2alf  2514  r2exf  2515  nfrabw  2678  cbvralfw  2719  cbvrexfw  2720  cbvralf  2721  cbvrexf  2722  cbvrab  2761  rmo3f  2961  nfccdeq  2987  sbcabel  3071  cbvcsbw  3088  cbvcsb  3089  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  dfss2f  3175  nfdif  3285  nfun  3320  nfin  3370  nfop  3825  nfiunxy  3943  nfiinxy  3944  nfiunya  3945  nfiinya  3946  cbviun  3954  cbviin  3955  iunxsngf  3995  cbvdisj  4021  nfdisjv  4023  disjiun  4029  nfmpt  4126  cbvmptf  4128  nffrfor  4384  onintrab2im  4555  tfis  4620  nfxp  4691  opeliunxp  4719  iunxpf  4815  elrnmpt1  4918  fvmptssdm  5649  nfmpo  5995  cbvmpox  6004  fmpox  6267  nffrec  6463  cc3  7351  nfsum1  11538  nfsum  11539  fsum2dlemstep  11616  fisumcom2  11620  nfcprod1  11736  nfcprod  11737  cbvprod  11740  fprod2dlemstep  11804  fprodcom2fi  11808  ctiunctlemudc  12679  ctiunctlemfo  12681