Theorem nfcri 2378

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

Syntax hints:  Ⅎwnf 1509   ∈ wcel 2203  Ⅎwnfc 2371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-cleq 2225  df-clel 2228  df-nfc 2373

This theorem is referenced by:  clelsb1f  2388  nfnfc  2391  nfeq  2392  nfel  2393  cleqf  2409  sbabel  2411  r2alf  2559  r2exf  2560  nfrabw  2724  cbvralfw  2766  cbvrexfw  2767  cbvralf  2768  cbvrexf  2769  cbvrab  2810  rmo3f  3013  nfccdeq  3039  sbcabel  3124  cbvcsbw  3141  cbvcsb  3142  cbvralcsf  3200  cbvrexcsf  3201  cbvreucsf  3202  cbvrabcsf  3203  dfss2f  3228  nfdif  3339  nfun  3374  nfin  3426  nfop  3898  nfiunxy  4016  nfiinxy  4017  nfiunya  4018  nfiinya  4019  cbviun  4027  cbviin  4028  iunxsngf  4068  cbvdisj  4094  nfdisjv  4096  disjiun  4103  nfmpt  4201  cbvmptf  4203  nffrfor  4468  onintrab2im  4639  tfis  4704  nfxp  4775  opeliunxp  4804  iunxpf  4902  elrnmpt1  5007  fvmptssdm  5761  nfmpo  6121  cbvmpox  6130  fmpox  6395  nffrec  6626  cc3  7581  nfsum1  12037  nfsum  12038  fsum2dlemstep  12116  fisumcom2  12120  nfcprod1  12236  nfcprod  12237  cbvprod  12240  fprod2dlemstep  12304  fprodcom2fi  12308  ctiunctlemudc  13180  ctiunctlemfo  13182