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  2658  cbvralfw  2695  cbvrexfw  2696  cbvralf  2697  cbvrexf  2698  cbvrab  2737  rmo3f  2936  nfccdeq  2962  sbcabel  3046  cbvcsbw  3063  cbvcsb  3064  cbvralcsf  3121  cbvrexcsf  3122  cbvreucsf  3123  cbvrabcsf  3124  dfss2f  3148  nfdif  3258  nfun  3293  nfin  3343  nfop  3796  nfiunxy  3914  nfiinxy  3915  nfiunya  3916  nfiinya  3917  cbviun  3925  cbviin  3926  iunxsngf  3966  cbvdisj  3992  nfdisjv  3994  disjiun  4000  nfmpt  4097  cbvmptf  4099  nffrfor  4350  onintrab2im  4519  tfis  4584  nfxp  4655  opeliunxp  4683  iunxpf  4777  elrnmpt1  4880  fvmptssdm  5602  nfmpo  5946  cbvmpox  5955  fmpox  6203  nffrec  6399  cc3  7269  nfsum1  11366  nfsum  11367  fsum2dlemstep  11444  fisumcom2  11448  nfcprod1  11564  nfcprod  11565  cbvprod  11568  fprod2dlemstep  11632  fprodcom2fi  11636  ctiunctlemudc  12440  ctiunctlemfo  12442