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 2150	1 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2114  Ⅎwnfc 2961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-10 2145  ax-11 2161  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  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  3429  cbvralf  3431  cbvrabw  3481  cbvrab  3482  rmo3f  3716  sbcabel  3850  cbvcsbw  3881  cbvcsb  3882  cbvrabcsfw  3912  cbvralcsf  3913  cbvreucsf  3915  cbvrabcsf  3916  nfdif  4090  nfun  4129  nfin  4181  nfiun  4935  nfiin  4936  nfiung  4937  nfiing  4938  cbviun  4947  cbviin  4948  cbviung  4949  cbviing  4950  cbvdisj  5027  nfdisjw  5029  nfdisj  5030  nfmpt  5149  cbvmptf  5151  cbvmptfg  5152  reusv2lem4  5288  nfxp  5574  opeliunxp  5605  iunxpf  5705  elrnmpt1  5816  nfmpo  7222  cbvmpox  7233  tfis  7555  fmpox  7751  nfsum1  15031  nfsum  15032  nfsumOLD  15033  fsum2dlem  15110  fsumcom2  15114  nfcprod  15250  cbvprod  15254  fprod2dlem  15319  fprodcom2  15323  gsum2d2lem  19076  dprd2d2  19149  ptbasfi  22172  restmetu  23163  ovoliunnul  24091  iundisj  24132  iunmbl2  24141  nfitg  24358  limciun  24477  reuxfrdf  30239  abrexss  30257  cbviunf  30293  iunin1f  30295  cbvdisjf  30307  disjabrex  30318  disjabrexf  30319  iundisjf  30325  ssrelf  30352  fmptcof2  30388  acunirnmpt2f  30392  iundisjfi  30505  locfinreflem  31114  esum2dlem  31358  oms0  31562  bnj1385  32111  bnj900  32208  bnj1014  32240  bnj1123  32265  bnj1228  32290  bnj1321  32306  bnj1384  32311  bnj1398  32313  bnj1408  32315  bnj1444  32322  bnj1445  32323  bnj1446  32324  bnj1449  32327  bnj1467  32333  bnj1518  32343  bj-nfcf  34258  mptsnunlem  34635  phpreu  34910  poimirlem26  34952  mbfposadd  34973  mpobi123f  35472  rababg  40023  ss2iundf  40094  binomcxplemnotnn0  40778  refsumcn  41377  iunssf  41442  cbvmpo2  41453  cbvmpo1  41454  iinssiin  41485  iinssf  41497  disjrnmpt2  41539  supxrleubrnmptf  41817  limcperiod  41999  limsupequzmptf  42102  dvnprodlem1  42321  stoweidlem16  42391  stoweidlem27  42402  stoweidlem28  42403  stoweidlem29  42404  stoweidlem31  42406  stoweidlem34  42409  stoweidlem35  42410  stoweidlem57  42432  stoweidlem59  42434  stirlinglem5  42453  fourierdlem16  42498  fourierdlem21  42503  fourierdlem22  42504  fourierdlem31  42513  fourierdlem48  42529  fourierdlem51  42532  fourierdlem53  42534  fourierdlem80  42561  fourierdlem93  42574  etransclem32  42641  opeliun2xp  44466  cbvmpox2  44469