Theorem nfcri 2213

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

Syntax hints:   F/wnf 1389   e. wcel 1433   F/_wnfc 2206

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 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-cleq 2074  df-clel 2077  df-nfc 2208

This theorem is referenced by:  nfnfc  2225  nfeq  2226  nfel  2227  cleqf  2242  sbabel  2244  r2alf  2383  r2exf  2384  nfrabxy  2534  cbvralf  2571  cbvrexf  2572  cbvrab  2599  nfccdeq  2813  sbcabel  2895  cbvcsb  2912  cbvralcsf  2964  cbvrexcsf  2965  cbvreucsf  2966  cbvrabcsf  2967  dfss2f  2990  nfdif  3093  nfun  3128  nfin  3172  nfop  3586  nfiunxy  3704  nfiinxy  3705  nfiunya  3706  nfiinya  3707  cbviun  3715  cbviin  3716  cbvdisj  3776  nfdisjv  3778  nfmpt  3870  nffrfor  4103  onintrab2im  4262  tfis  4324  nfxp  4389  opeliunxp  4413  iunxpf  4502  elrnmpt1  4603  fvmptssdm  5276  nfmpt2  5593  cbvmpt2x  5602  fmpt2x  5846  nffrec  6005  nfsum1  10193  nfsum  10194