Theorem nfcri 2758

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

Syntax hints:   F/wnf 1708   e. wcel 1990   F/_wnfc 2751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-cleq 2615  df-clel 2618  df-nfc 2753

This theorem is referenced by:  clelsb3f  2768  nfnfcALT  2775  sbabel  2793  r2alf  2938  nfrab  3123  cbvralf  3165  cbvrab  3198  nfccdeq  3433  sbcabel  3517  cbvcsb  3538  cbvralcsf  3565  cbvreucsf  3567  cbvrabcsf  3568  dfss2f  3594  nfdif  3731  nfun  3769  nfin  3820  nfiun  4548  nfiin  4549  cbviun  4557  cbviin  4558  cbvdisj  4630  nfdisj  4632  nfmpt  4746  cbvmptf  4748  reusv2lem4  4872  nfxp  5142  opeliunxp  5170  iunxpf  5270  elrnmpt1  5374  nfmpt2  6724  cbvmpt2x  6733  tfis  7054  fmpt2x  7236  nfsum1  14420  nfsum  14421  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  nfcprod  14641  cbvprod  14645  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  gsum2d2lem  18372  dprd2d2  18443  ptbasfi  21384  restmetu  22375  ovoliunnul  23275  iundisj  23316  iunmbl2  23325  nfitg  23541  limciun  23658  rmo3f  29335  abrexss  29350  cbviunf  29372  iunin1f  29374  iunxsngf  29375  cbvdisjf  29385  disjabrex  29395  disjabrexf  29396  iundisjf  29402  ssrelf  29425  fmptcof2  29457  acunirnmpt2f  29461  iundisjfi  29555  locfinreflem  29907  esum2dlem  30154  oms0  30359  bnj1385  30903  bnj900  30999  bnj1014  31030  bnj1123  31054  bnj1228  31079  bnj1321  31095  bnj1384  31100  bnj1398  31102  bnj1408  31104  bnj1444  31111  bnj1445  31112  bnj1446  31113  bnj1449  31116  bnj1467  31122  bnj1518  31132  bj-nfcf  32920  mptsnunlem  33185  phpreu  33393  poimirlem26  33435  mbfposadd  33457  csbgfi  33935  mpt2bi123f  33971  rababg  37879  ss2iundf  37951  binomcxplemnotnn0  38555  refsumcn  39189  iunxsngf2  39230  iunssf  39263  cbvmpt22  39277  cbvmpt21  39278  wessf1ornlem  39371  disjrnmpt2  39375  supxrleubrnmptf  39680  limcperiod  39860  limsupequzmptf  39963  dvnprodlem1  40161  stoweidlem16  40233  stoweidlem27  40244  stoweidlem28  40245  stoweidlem29  40246  stoweidlem31  40248  stoweidlem34  40251  stoweidlem35  40252  stoweidlem57  40274  stoweidlem59  40276  stirlinglem5  40295  fourierdlem16  40340  fourierdlem21  40345  fourierdlem22  40346  fourierdlem31  40355  fourierdlem48  40371  fourierdlem51  40374  fourierdlem53  40376  fourierdlem80  40403  fourierdlem93  40416  etransclem32  40483  opeliun2xp  42111  cbvmpt2x2  42114