Theorem nfcri 2971

Description: Consequence of the not-free predicate. (Note that unlike nfcr 2966, this does not require 𝑦 and 𝐴 to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfcri.1	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nfcri	⊢ Ⅎ𝑥 𝑦 ∈ 𝐴

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)

Proof of Theorem nfcri

Step	Hyp	Ref	Expression
1		nfcri.1	. . 3 ⊢ Ⅎ𝑥𝐴
2	1	nfcrii 2970	. 2 ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
3	2	nf5i 2146	1 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴

Syntax hints:  Ⅎwnf 1780   ∈ wcel 2110  Ⅎwnfc 2961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-10 2141  ax-11 2157  ax-12 2173

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-sb 2066  df-clel 2893  df-nfc 2963

This theorem is referenced by:  clelsb3fw  2981  clelsb3f  2982  clelsb3fOLD  2983  sbabel  3015  r2alf  3222  nfrabw  3385  nfrab  3386  cbvralfw  3437  cbvralf  3439  cbvrabw  3489  cbvrab  3490  rmo3f  3724  sbcabel  3860  cbvcsbw  3892  cbvcsb  3893  cbvrabcsfw  3923  cbvralcsf  3924  cbvreucsf  3926  cbvrabcsf  3927  nfdif  4101  nfun  4140  nfin  4192  nfiun  4941  nfiin  4942  nfiung  4943  nfiing  4944  cbviun  4953  cbviin  4954  cbviung  4955  cbviing  4956  cbvdisj  5033  nfdisjw  5035  nfdisj  5036  nfmpt  5155  cbvmptf  5157  cbvmptfg  5158  reusv2lem4  5293  nfxp  5582  opeliunxp  5613  iunxpf  5713  elrnmpt1  5824  nfmpo  7230  cbvmpox  7241  tfis  7563  fmpox  7759  nfsum1  15040  nfsumw  15041  nfsum  15042  fsum2dlem  15119  fsumcom2  15123  nfcprod  15259  cbvprod  15263  fprod2dlem  15328  fprodcom2  15332  gsum2d2lem  19087  dprd2d2  19160  ptbasfi  22183  restmetu  23174  ovoliunnul  24102  iundisj  24143  iunmbl2  24152  nfitg  24369  limciun  24486  reuxfrdf  30249  abrexss  30266  cbviunf  30301  iunin1f  30303  cbvdisjf  30315  disjabrex  30326  disjabrexf  30327  iundisjf  30333  ssrelf  30360  fmptcof2  30396  acunirnmpt2f  30400  iundisjfi  30513  locfinreflem  31099  esum2dlem  31346  oms0  31550  bnj1385  32099  bnj900  32196  bnj1014  32228  bnj1123  32253  bnj1228  32278  bnj1321  32294  bnj1384  32299  bnj1398  32301  bnj1408  32303  bnj1444  32310  bnj1445  32311  bnj1446  32312  bnj1449  32315  bnj1467  32321  bnj1518  32331  bj-nfcf  34237  mptsnunlem  34613  phpreu  34870  poimirlem26  34912  mbfposadd  34933  mpobi123f  35434  rababg  39926  ss2iundf  39997  binomcxplemnotnn0  40681  refsumcn  41280  iunssf  41345  cbvmpo2  41356  cbvmpo1  41357  iinssiin  41388  iinssf  41400  disjrnmpt2  41442  supxrleubrnmptf  41720  limcperiod  41902  limsupequzmptf  42005  dvnprodlem1  42224  stoweidlem16  42295  stoweidlem27  42306  stoweidlem28  42307  stoweidlem29  42308  stoweidlem31  42310  stoweidlem34  42313  stoweidlem35  42314  stoweidlem57  42336  stoweidlem59  42338  stirlinglem5  42357  fourierdlem16  42402  fourierdlem21  42407  fourierdlem22  42408  fourierdlem31  42417  fourierdlem48  42433  fourierdlem51  42436  fourierdlem53  42438  fourierdlem80  42465  fourierdlem93  42478  etransclem32  42545  opeliun2xp  44375  cbvmpox2  44378