Theorem nfcri 2222

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

Syntax hints:   F/wnf 1394   e. wcel 1438   F/_wnfc 2215

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-cleq 2081  df-clel 2084  df-nfc 2217

This theorem is referenced by:  clelsb3f  2232  nfnfc  2235  nfeq  2236  nfel  2237  cleqf  2252  sbabel  2254  r2alf  2395  r2exf  2396  nfrabxy  2547  cbvralf  2584  cbvrexf  2585  cbvrab  2617  rmo3f  2812  nfccdeq  2838  sbcabel  2920  cbvcsb  2937  cbvralcsf  2990  cbvrexcsf  2991  cbvreucsf  2992  cbvrabcsf  2993  dfss2f  3016  nfdif  3121  nfun  3156  nfin  3206  nfop  3638  nfiunxy  3756  nfiinxy  3757  nfiunya  3758  nfiinya  3759  cbviun  3767  cbviin  3768  iunxsngf  3807  cbvdisj  3832  nfdisjv  3834  disjiun  3840  nfmpt  3930  cbvmptf  3932  nffrfor  4175  onintrab2im  4335  tfis  4398  nfxp  4464  opeliunxp  4493  iunxpf  4584  elrnmpt1  4686  fvmptssdm  5387  nfmpt2  5717  cbvmpt2x  5726  fmpt2x  5970  nffrec  6161  nfsum1  10745  nfsum  10746  fsum2dlemstep  10828  fisumcom2  10832