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

Theorem nfcri 2534
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2532, 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 2533 . 2  |-  ( y  e.  A  ->  A. x  y  e.  A )
32nfi 1557 1  |-  F/ x  y  e.  A
Colors of variables: wff set class
Syntax hints:   F/wnf 1550    e. wcel 1721   F/_wnfc 2527
This theorem is referenced by:  nfnfc  2546  nfeq  2547  nfel  2548  cleqf  2564  sbabel  2566  r2alf  2701  r2exf  2702  nfrab  2849  cbvralf  2886  cbvrab  2914  nfccdeq  3119  sbcabel  3198  cbvcsb  3215  cbvralcsf  3271  cbvreucsf  3273  cbvrabcsf  3274  dfss2f  3299  nfdif  3428  nfun  3463  nfin  3507  nfiun  4079  nfiin  4080  cbviun  4088  cbviin  4089  cbvdisj  4152  nfdisj  4154  nfmpt  4257  reusv2lem4  4686  tfis  4793  nfxp  4863  opeliunxp  4888  iunxpf  4980  elrnmpt1  5078  nfmpt2  6101  cbvmpt2x  6109  fmpt2x  6376  nfsum  12440  cbvsum  12444  fsum2dlem  12509  fsumcom2  12513  gsum2d2lem  15502  dprd2d2  15557  ptbasfi  17566  restmetu  18570  ovoliunnul  19356  iundisj  19395  iunmbl2  19404  nfitg  19619  limciun  19734  clelsb3f  23924  rmo3f  23935  abrexss  23946  cbvdisjf  23968  disjabrex  23977  disjabrexf  23978  iundisjf  23982  cbvmptf  24021  fmptcof2  24029  iundisjfi  24105  nfcprod  25190  cbvprod  25194  fprod2dlem  25257  fprodcom2  25261  refsumcn  27568  stoweidlem16  27632  stoweidlem27  27643  stoweidlem28  27644  stoweidlem29  27645  stoweidlem31  27647  stoweidlem34  27650  stoweidlem35  27651  stoweidlem57  27673  stoweidlem59  27675  stirlinglem5  27694  bnj1385  28910  bnj1476  28924  bnj900  29006  bnj1014  29037  bnj1123  29061  bnj1228  29086  bnj1321  29102  bnj1384  29107  bnj1398  29109  bnj1408  29111  bnj1444  29118  bnj1445  29119  bnj1446  29120  bnj1449  29123  bnj1467  29129  bnj1518  29139
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2397  df-clel 2400  df-nfc 2529
  Copyright terms: Public domain W3C validator