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

Theorem nfcri 2518
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2516, 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 2517 . 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 1717   F/_wnfc 2511
This theorem is referenced by:  nfnfc  2530  nfeq  2531  nfel  2532  cleqf  2548  sbabel  2550  r2alf  2685  r2exf  2686  nfrab  2833  cbvralf  2870  cbvrab  2898  nfccdeq  3103  sbcabel  3182  cbvcsb  3199  cbvralcsf  3255  cbvreucsf  3257  cbvrabcsf  3258  dfss2f  3283  nfdif  3412  nfun  3447  nfin  3491  nfiun  4062  nfiin  4063  cbviun  4070  cbviin  4071  cbvdisj  4134  nfdisj  4136  nfmpt  4239  reusv2lem4  4668  tfis  4775  nfxp  4845  opeliunxp  4870  iunxpf  4962  elrnmpt1  5060  nfmpt2  6082  cbvmpt2x  6090  fmpt2x  6357  nfsum  12413  cbvsum  12417  fsum2dlem  12482  fsumcom2  12486  gsum2d2lem  15475  dprd2d2  15530  ptbasfi  17535  restmetu  18490  ovoliunnul  19271  iundisj  19310  iunmbl2  19319  nfitg  19534  limciun  19649  clelsb3f  23816  rmo3f  23827  abrexss  23838  cbvdisjf  23860  disjabrex  23869  disjabrexf  23870  iundisjf  23873  cbvmptf  23911  fmptcof2  23919  iundisjfi  23991  nfcprod  25017  cbvprod  25021  refsumcn  27370  stoweidlem16  27434  stoweidlem27  27445  stoweidlem28  27446  stoweidlem29  27447  stoweidlem31  27449  stoweidlem34  27452  stoweidlem35  27453  stoweidlem57  27475  stoweidlem59  27477  stirlinglem5  27496  bnj1385  28543  bnj1476  28557  bnj900  28639  bnj1014  28670  bnj1123  28694  bnj1228  28719  bnj1321  28735  bnj1384  28740  bnj1398  28742  bnj1408  28744  bnj1444  28751  bnj1445  28752  bnj1446  28753  bnj1449  28756  bnj1467  28762  bnj1518  28772
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2381  df-clel 2384  df-nfc 2513
  Copyright terms: Public domain W3C validator