Theorem nfcri 2963

Description: Consequence of the not-free predicate. (Note that unlike nfcr 2961, 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 2962	. 2 ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
3	2	nf5i 2197	1 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴

Syntax hints:  Ⅎwnf 1882   ∈ wcel 2164  Ⅎwnfc 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clel 2821  df-nfc 2958

This theorem is referenced by:  clelsb3f  2973  nfnfcALT  2980  sbabel  2998  r2alf  3147  nfrab  3334  cbvralf  3377  cbvrab  3411  rmo3f  3628  nfccdeq  3660  sbcabel  3741  cbvcsb  3762  cbvralcsf  3789  cbvreucsf  3791  cbvrabcsf  3792  dfss2f  3818  nfdif  3958  nfun  3996  nfin  4045  nfiun  4768  nfiin  4769  cbviun  4777  cbviin  4778  iunxsngf  4824  cbvdisj  4851  nfdisj  4853  nfmpt  4969  cbvmptf  4971  reusv2lem4  5101  nfxp  5375  opeliunxp  5403  iunxpf  5503  elrnmpt1  5607  nfmpt2  6984  cbvmpt2x  6993  tfis  7315  fmpt2x  7499  nfsum1  14797  nfsum  14798  fsum2dlem  14876  fsumcom2  14880  nfcprod  15014  cbvprod  15018  fprod2dlem  15083  fprodcom2  15087  gsum2d2lem  18725  dprd2d2  18797  ptbasfi  21755  restmetu  22745  ovoliunnul  23673  iundisj  23714  iunmbl2  23723  nfitg  23940  limciun  24057  abrexss  29887  cbviunf  29909  iunin1f  29911  cbvdisjf  29921  disjabrex  29931  disjabrexf  29932  iundisjf  29938  ssrelf  29963  fmptcof2  29995  acunirnmpt2f  29999  iundisjfi  30091  locfinreflem  30441  esum2dlem  30688  oms0  30893  bnj1385  31438  bnj900  31534  bnj1014  31565  bnj1123  31589  bnj1228  31614  bnj1321  31630  bnj1384  31635  bnj1398  31637  bnj1408  31639  bnj1444  31646  bnj1445  31647  bnj1446  31648  bnj1449  31651  bnj1467  31657  bnj1518  31667  bj-nfcf  33436  mptsnunlem  33724  phpreu  33929  poimirlem26  33972  mbfposadd  33993  csbgfi  34468  mpt2bi123f  34504  rababg  38713  ss2iundf  38785  binomcxplemnotnn0  39388  refsumcn  40000  iunxsngf2  40040  iunssf  40073  cbvmpt22  40087  cbvmpt21  40088  wessf1ornlem  40172  disjrnmpt2  40176  supxrleubrnmptf  40468  limcperiod  40648  limsupequzmptf  40751  dvnprodlem1  40949  stoweidlem16  41020  stoweidlem27  41031  stoweidlem28  41032  stoweidlem29  41033  stoweidlem31  41035  stoweidlem34  41038  stoweidlem35  41039  stoweidlem57  41061  stoweidlem59  41063  stirlinglem5  41082  fourierdlem16  41127  fourierdlem21  41132  fourierdlem22  41133  fourierdlem31  41142  fourierdlem48  41158  fourierdlem51  41161  fourierdlem53  41163  fourierdlem80  41190  fourierdlem93  41203  etransclem32  41270  opeliun2xp  42951  cbvmpt2x2  42954