Theorem nfcri 2380

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

Syntax hints:  Ⅎwnf 1509   ∈ wcel 2205  Ⅎwnfc 2373

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-cleq 2227  df-clel 2230  df-nfc 2375

This theorem is referenced by:  clelsb1f  2390  nfnfc  2393  nfeq  2394  nfel  2395  cleqf  2411  sbabel  2413  r2alf  2561  r2exf  2562  nfrabw  2727  cbvralfw  2769  cbvrexfw  2770  cbvralf  2771  cbvrexf  2772  cbvrab  2813  rmo3f  3017  nfccdeq  3043  sbcabel  3128  cbvcsbw  3145  cbvcsb  3146  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  dfssf  3232  dfss2f  3233  nfdif  3344  nfun  3379  nfin  3431  nfop  3904  nfiunxy  4022  nfiinxy  4023  nfiunya  4024  nfiinya  4025  cbviun  4033  cbviin  4034  iunxsngf  4074  cbvdisj  4100  nfdisjv  4102  disjiun  4109  nfmpt  4207  cbvmptf  4209  nffrfor  4474  onintrab2im  4645  tfis  4710  nfxp  4781  opeliunxp  4810  iunxpf  4908  elrnmpt1  5013  fvmptssdm  5767  nfmpo  6130  cbvmpox  6139  abrexss  6331  fmpox  6409  nffrec  6640  cc3  7598  nfsum1  12066  nfsum  12067  fsum2dlemstep  12145  fisumcom2  12149  nfcprod1  12265  nfcprod  12266  cbvprod  12269  fprod2dlemstep  12333  fprodcom2fi  12337  ctiunctlemudc  13272  ctiunctlemfo  13274