Theorem nfcri 2313

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

Syntax hints:  Ⅎwnf 1460   ∈ wcel 2148  Ⅎwnfc 2306

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308

This theorem is referenced by:  clelsb1f  2323  nfnfc  2326  nfeq  2327  nfel  2328  cleqf  2344  sbabel  2346  r2alf  2494  r2exf  2495  nfrabxy  2657  cbvralfw  2694  cbvrexfw  2695  cbvralf  2696  cbvrexf  2697  cbvrab  2735  rmo3f  2934  nfccdeq  2960  sbcabel  3044  cbvcsbw  3061  cbvcsb  3062  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  dfss2f  3146  nfdif  3256  nfun  3291  nfin  3341  nfop  3794  nfiunxy  3912  nfiinxy  3913  nfiunya  3914  nfiinya  3915  cbviun  3923  cbviin  3924  iunxsngf  3963  cbvdisj  3989  nfdisjv  3991  disjiun  3997  nfmpt  4094  cbvmptf  4096  nffrfor  4347  onintrab2im  4516  tfis  4581  nfxp  4652  opeliunxp  4680  iunxpf  4774  elrnmpt1  4877  fvmptssdm  5599  nfmpo  5941  cbvmpox  5950  fmpox  6198  nffrec  6394  cc3  7264  nfsum1  11357  nfsum  11358  fsum2dlemstep  11435  fisumcom2  11439  nfcprod1  11555  nfcprod  11556  cbvprod  11559  fprod2dlemstep  11623  fprodcom2fi  11627  ctiunctlemudc  12430  ctiunctlemfo  12432