Theorem nfcri 2273

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

Syntax hints:   F/wnf 1436   e. wcel 1480   F/_wnfc 2266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-cleq 2130  df-clel 2133  df-nfc 2268

This theorem is referenced by:  clelsb3f  2283  nfnfc  2286  nfeq  2287  nfel  2288  cleqf  2303  sbabel  2305  r2alf  2450  r2exf  2451  nfrabxy  2609  cbvralf  2646  cbvrexf  2647  cbvrab  2679  rmo3f  2876  nfccdeq  2902  sbcabel  2985  cbvcsbw  3002  cbvcsb  3003  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  dfss2f  3083  nfdif  3192  nfun  3227  nfin  3277  nfop  3716  nfiunxy  3834  nfiinxy  3835  nfiunya  3836  nfiinya  3837  cbviun  3845  cbviin  3846  iunxsngf  3885  cbvdisj  3911  nfdisjv  3913  disjiun  3919  nfmpt  4015  cbvmptf  4017  nffrfor  4265  onintrab2im  4429  tfis  4492  nfxp  4561  opeliunxp  4589  iunxpf  4682  elrnmpt1  4785  fvmptssdm  5498  nfmpo  5833  cbvmpox  5842  fmpox  6091  nffrec  6286  nfsum1  11118  nfsum  11119  fsum2dlemstep  11196  fisumcom2  11200  nfcprod1  11316  nfcprod  11317  cbvprod  11320  ctiunctlemudc  11939  ctiunctlemfo  11941