Theorem nfcri 2333

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

Syntax hints:  Ⅎwnf 1474   ∈ wcel 2167  Ⅎwnfc 2326

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-cleq 2189  df-clel 2192  df-nfc 2328

This theorem is referenced by:  clelsb1f  2343  nfnfc  2346  nfeq  2347  nfel  2348  cleqf  2364  sbabel  2366  r2alf  2514  r2exf  2515  nfrabw  2678  cbvralfw  2719  cbvrexfw  2720  cbvralf  2721  cbvrexf  2722  cbvrab  2761  rmo3f  2961  nfccdeq  2987  sbcabel  3071  cbvcsbw  3088  cbvcsb  3089  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  dfss2f  3174  nfdif  3284  nfun  3319  nfin  3369  nfop  3824  nfiunxy  3942  nfiinxy  3943  nfiunya  3944  nfiinya  3945  cbviun  3953  cbviin  3954  iunxsngf  3994  cbvdisj  4020  nfdisjv  4022  disjiun  4028  nfmpt  4125  cbvmptf  4127  nffrfor  4383  onintrab2im  4554  tfis  4619  nfxp  4690  opeliunxp  4718  iunxpf  4814  elrnmpt1  4917  fvmptssdm  5646  nfmpo  5991  cbvmpox  6000  fmpox  6258  nffrec  6454  cc3  7335  nfsum1  11521  nfsum  11522  fsum2dlemstep  11599  fisumcom2  11603  nfcprod1  11719  nfcprod  11720  cbvprod  11723  fprod2dlemstep  11787  fprodcom2fi  11791  ctiunctlemudc  12654  ctiunctlemfo  12656