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

Theorem nfcri 2563
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2561, 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 2562 . 2  |-  ( y  e.  A  ->  A. x  y  e.  A )
32nfi 1599 1  |-  F/ x  y  e.  A
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1592    e. wcel 1755   F/_wnfc 2556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-cleq 2426  df-clel 2429  df-nfc 2558
This theorem is referenced by:  nfnfc  2575  nfeq  2576  nfel  2577  cleqf  2593  sbabel  2595  r2alf  2740  r2exf  2741  nfrab  2892  cbvralf  2931  cbvrab  2960  nfccdeq  3173  sbcabel  3263  cbvcsb  3281  cbvralcsf  3307  cbvreucsf  3309  cbvrabcsf  3310  dfss2f  3335  nfdif  3465  nfun  3500  nfin  3545  nfiun  4186  nfiin  4187  cbviun  4195  cbviin  4196  cbvdisj  4260  nfdisj  4262  nfmpt  4368  reusv2lem4  4484  nfxp  4853  opeliunxp  4877  iunxpf  4975  elrnmpt1  5075  nfmpt2  6144  cbvmpt2x  6153  tfis  6454  fmpt2x  6629  fsum2dlem  13220  fsumcom2  13224  gsum2d2lem  16438  dprd2d2  16516  ptbasfi  18995  restmetu  20003  ovoliunnul  20831  iundisj  20870  iunmbl2  20879  nfitg  21093  limciun  21210  clelsb3f  25686  rmo3f  25702  abrexss  25716  cbvdisjf  25740  disjabrex  25749  disjabrexf  25750  iundisjf  25754  cbvmptf  25794  fmptcof2  25802  iundisjfi  25902  nfcprod  27270  cbvprod  27274  fprod2dlem  27337  fprodcom2  27341  csbgfi  28780  refsumcn  29594  stoweidlem16  29654  stoweidlem27  29665  stoweidlem28  29666  stoweidlem29  29667  stoweidlem31  29669  stoweidlem34  29672  stoweidlem35  29673  stoweidlem57  29695  stoweidlem59  29697  stirlinglem5  29716  rabasiun  30073  opeliun2xp  30562  cbvmpt2x2  30567  bnj1385  31525  bnj1476  31539  bnj900  31621  bnj1014  31652  bnj1123  31676  bnj1228  31701  bnj1321  31717  bnj1384  31722  bnj1398  31724  bnj1408  31726  bnj1444  31733  bnj1445  31734  bnj1446  31735  bnj1449  31738  bnj1467  31744  bnj1518  31754
  Copyright terms: Public domain W3C validator