Theorem nfcri 2343

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

Syntax hints:  Ⅎwnf 1484   ∈ wcel 2177  Ⅎwnfc 2336

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-cleq 2199  df-clel 2202  df-nfc 2338

This theorem is referenced by:  clelsb1f  2353  nfnfc  2356  nfeq  2357  nfel  2358  cleqf  2374  sbabel  2376  r2alf  2524  r2exf  2525  nfrabw  2688  cbvralfw  2729  cbvrexfw  2730  cbvralf  2731  cbvrexf  2732  cbvrab  2771  rmo3f  2972  nfccdeq  2998  sbcabel  3082  cbvcsbw  3099  cbvcsb  3100  cbvralcsf  3158  cbvrexcsf  3159  cbvreucsf  3160  cbvrabcsf  3161  dfss2f  3186  nfdif  3296  nfun  3331  nfin  3381  nfop  3838  nfiunxy  3956  nfiinxy  3957  nfiunya  3958  nfiinya  3959  cbviun  3967  cbviin  3968  iunxsngf  4008  cbvdisj  4034  nfdisjv  4036  disjiun  4043  nfmpt  4141  cbvmptf  4143  nffrfor  4400  onintrab2im  4571  tfis  4636  nfxp  4707  opeliunxp  4735  iunxpf  4831  elrnmpt1  4935  fvmptssdm  5674  nfmpo  6024  cbvmpox  6033  fmpox  6296  nffrec  6492  cc3  7393  nfsum1  11717  nfsum  11718  fsum2dlemstep  11795  fisumcom2  11799  nfcprod1  11915  nfcprod  11916  cbvprod  11919  fprod2dlemstep  11983  fprodcom2fi  11987  ctiunctlemudc  12858  ctiunctlemfo  12860