Theorem nfcri 2290

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

Syntax hints:  Ⅎwnf 1437   ∈ wcel 2125  Ⅎwnfc 2283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1740  df-cleq 2147  df-clel 2150  df-nfc 2285

This theorem is referenced by:  clelsb3f  2300  nfnfc  2303  nfeq  2304  nfel  2305  cleqf  2321  sbabel  2323  r2alf  2471  r2exf  2472  nfrabxy  2634  cbvralf  2671  cbvrexf  2672  cbvrab  2707  rmo3f  2905  nfccdeq  2931  sbcabel  3014  cbvcsbw  3031  cbvcsb  3032  cbvralcsf  3089  cbvrexcsf  3090  cbvreucsf  3091  cbvrabcsf  3092  dfss2f  3115  nfdif  3224  nfun  3259  nfin  3309  nfop  3753  nfiunxy  3871  nfiinxy  3872  nfiunya  3873  nfiinya  3874  cbviun  3882  cbviin  3883  iunxsngf  3922  cbvdisj  3948  nfdisjv  3950  disjiun  3956  nfmpt  4052  cbvmptf  4054  nffrfor  4303  onintrab2im  4471  tfis  4536  nfxp  4606  opeliunxp  4634  iunxpf  4727  elrnmpt1  4830  fvmptssdm  5545  nfmpo  5880  cbvmpox  5889  fmpox  6138  nffrec  6333  cc3  7167  nfsum1  11230  nfsum  11231  fsum2dlemstep  11308  fisumcom2  11312  nfcprod1  11428  nfcprod  11429  cbvprod  11432  fprod2dlemstep  11496  fprodcom2fi  11500  ctiunctlemudc  12125  ctiunctlemfo  12127