MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfcri Unicode version

Theorem nfcri 2415
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2413, this does not require  y and  A to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfcri.1  |-  F/_ x A
Assertion
Ref Expression
nfcri  |-  F/ x  y  e.  A
Distinct variable group:    x, y
Allowed substitution hints:    A( x, y)

Proof of Theorem nfcri
StepHypRef Expression
1 nfcri.1 . . 3  |-  F/_ x A
21nfcrii 2414 . 2  |-  ( y  e.  A  ->  A. x  y  e.  A )
32nfi 1539 1  |-  F/ x  y  e.  A
Colors of variables: wff set class
Syntax hints:   F/wnf 1532    e. wcel 1685   F/_wnfc 2408
This theorem is referenced by:  nfnfc  2427  nfeq  2428  nfel  2429  cleqf  2445  sbabel  2447  r2alf  2580  r2exf  2581  nfrab  2723  cbvralf  2760  cbvrab  2788  nfccdeq  2991  sbcabel  3070  cbvcsb  3087  cbvralcsf  3145  cbvreucsf  3147  cbvrabcsf  3148  dfss2f  3173  nfdif  3299  nfun  3333  nfin  3377  nfiun  3933  nfiin  3934  cbviun  3941  cbviin  3942  cbvdisj  4005  nfdisj  4007  nfmpt  4110  tfis  4645  nfxp  4715  opeliunxp  4740  iunxpf  4832  nfmpt2  5878  cbvmpt2x  5886  nfsum  12159  cbvsum  12163  ptbasfi  17271  nfitg  19124  limciun  19239  nfprod1  24710  nfprod  24711  bnj1385  28133  bnj1476  28147  bnj900  28229  bnj1014  28260  bnj1123  28284  bnj1228  28309  bnj1321  28325  bnj1384  28330  bnj1398  28332  bnj1408  28334  bnj1444  28341  bnj1445  28342  bnj1446  28343  bnj1449  28346  bnj1467  28352  bnj1518  28362
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-cleq 2278  df-clel 2281  df-nfc 2410
  Copyright terms: Public domain W3C validator