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

Theorem nfcri 2386
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2384, 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 2385 . 2  |-  ( y  e.  A  ->  A. x  y  e.  A )
32nfi 1556 1  |-  F/ x  y  e.  A
Colors of variables: wff set class
Syntax hints:   F/wnf 1539    e. wcel 1621   F/_wnfc 2379
This theorem is referenced by:  nfnfc  2398  nfeq  2399  nfel  2400  cleqf  2416  sbabel  2418  r2alf  2549  r2exf  2550  nfrab  2689  cbvralf  2712  cbvrab  2738  nfccdeq  2933  sbcabel  3012  cbvcsb  3027  cbvralcsf  3085  cbvreucsf  3087  cbvrabcsf  3088  dfss2f  3113  nfdif  3239  nfun  3273  nfin  3317  nfiun  3872  nfiin  3873  cbviun  3880  cbviin  3881  cbvdisj  3943  nfdisj  3945  nfmpt  4048  tfis  4582  nfxp  4668  opeliunxp  4693  iunxpf  4785  nfmpt2  5815  cbvmpt2x  5823  nfsum  12094  cbvsum  12098  ptbasfi  17203  nfitg  19056  limciun  19171  nfprod1  24642  nfprod  24643  bnj1385  27877  bnj1476  27891  bnj900  27973  bnj1014  28004  bnj1123  28028  bnj1228  28053  bnj1321  28069  bnj1384  28074  bnj1398  28076  bnj1408  28078  bnj1444  28085  bnj1445  28086  bnj1446  28087  bnj1449  28090  bnj1467  28096  bnj1518  28106
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-cleq 2249  df-clel 2252  df-nfc 2381
  Copyright terms: Public domain W3C validator