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

Theorem nfcri 2578
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2576, 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 2577 . 2  |-  ( y  e.  A  ->  A. x  y  e.  A )
32nfi 1596 1  |-  F/ x  y  e.  A
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1589    e. wcel 1756   F/_wnfc 2571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-cleq 2436  df-clel 2439  df-nfc 2573
This theorem is referenced by:  nfnfc  2590  nfeq  2591  nfel  2592  cleqf  2608  sbabel  2610  r2alf  2755  r2exf  2756  nfrab  2907  cbvralf  2946  cbvrab  2975  nfccdeq  3189  sbcabel  3280  cbvcsb  3298  cbvralcsf  3324  cbvreucsf  3326  cbvrabcsf  3327  dfss2f  3352  nfdif  3482  nfun  3517  nfin  3562  nfiun  4203  nfiin  4204  cbviun  4212  cbviin  4213  cbvdisj  4277  nfdisj  4279  nfmpt  4385  reusv2lem4  4501  nfxp  4871  opeliunxp  4895  iunxpf  4993  elrnmpt1  5093  nfmpt2  6160  cbvmpt2x  6169  tfis  6470  fmpt2x  6645  fsum2dlem  13242  fsumcom2  13246  gsum2d2lem  16470  dprd2d2  16548  ptbasfi  19159  restmetu  20167  ovoliunnul  20995  iundisj  21034  iunmbl2  21043  nfitg  21257  limciun  21374  clelsb3f  25869  rmo3f  25884  abrexss  25898  cbvdisjf  25922  disjabrex  25931  disjabrexf  25932  iundisjf  25936  cbvmptf  25976  fmptcof2  25984  iundisjfi  26085  nfcprod  27429  cbvprod  27433  fprod2dlem  27496  fprodcom2  27500  csbgfi  28944  mpt2bi123f  28980  refsumcn  29757  stoweidlem16  29816  stoweidlem27  29827  stoweidlem28  29828  stoweidlem29  29829  stoweidlem31  29831  stoweidlem34  29834  stoweidlem35  29835  stoweidlem57  29857  stoweidlem59  29859  stirlinglem5  29878  rabasiun  30235  opeliun2xp  30725  cbvmpt2x2  30731  bnj1385  31831  bnj1476  31845  bnj900  31927  bnj1014  31958  bnj1123  31982  bnj1228  32007  bnj1321  32023  bnj1384  32028  bnj1398  32030  bnj1408  32032  bnj1444  32039  bnj1445  32040  bnj1446  32041  bnj1449  32044  bnj1467  32050  bnj1518  32060
  Copyright terms: Public domain W3C validator