Theorem nfcri 2172

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

Syntax hints:   F/wnf 1349   e. wcel 1393   F/_wnfc 2165

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-cleq 2033  df-clel 2036  df-nfc 2167

This theorem is referenced by:  nfnfc  2184  nfeq  2185  nfel  2186  cleqf  2201  sbabel  2203  r2alf  2341  r2exf  2342  nfrabxy  2490  cbvralf  2527  cbvrexf  2528  cbvrab  2555  nfccdeq  2762  sbcabel  2839  cbvcsb  2856  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  dfss2f  2936  nfdif  3065  nfun  3099  nfin  3143  nfop  3565  nfiunxy  3683  nfiinxy  3684  nfiunya  3685  nfiinya  3686  cbviun  3694  cbviin  3695  cbvdisj  3755  nfdisjv  3757  nfmpt  3849  nffrfor  4085  onintrab2im  4244  tfis  4306  nfxp  4371  opeliunxp  4395  iunxpf  4484  elrnmpt1  4585  fvmptssdm  5255  nfmpt2  5573  cbvmpt2x  5582  fmpt2x  5826  nffrec  5982  nfsum1  9875  nfsum  9876