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

Theorem nfcri 2426
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2424, 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 2425 . 2  |-  ( y  e.  A  ->  A. x  y  e.  A )
32nfi 1541 1  |-  F/ x  y  e.  A
Colors of variables: wff set class
Syntax hints:   F/wnf 1534    e. wcel 1696   F/_wnfc 2419
This theorem is referenced by:  nfnfc  2438  nfeq  2439  nfel  2440  cleqf  2456  sbabel  2458  r2alf  2591  r2exf  2592  nfrab  2734  cbvralf  2771  cbvrab  2799  nfccdeq  3002  sbcabel  3081  cbvcsb  3098  cbvralcsf  3156  cbvreucsf  3158  cbvrabcsf  3159  dfss2f  3184  nfdif  3310  nfun  3344  nfin  3388  nfiun  3947  nfiin  3948  cbviun  3955  cbviin  3956  cbvdisj  4019  nfdisj  4021  nfmpt  4124  tfis  4661  nfxp  4731  opeliunxp  4756  iunxpf  4848  nfmpt2  5932  cbvmpt2x  5940  nfsum  12180  cbvsum  12184  ptbasfi  17292  nfitg  19145  limciun  19260  cbvdisjf  23365  disjabrex  23374  disjabrexf  23375  cbvcprod  24137  nfprod1  25413  nfprod  25414  bnj1385  29181  bnj1476  29195  bnj900  29277  bnj1014  29308  bnj1123  29332  bnj1228  29357  bnj1321  29373  bnj1384  29378  bnj1398  29380  bnj1408  29382  bnj1444  29389  bnj1445  29390  bnj1446  29391  bnj1449  29394  bnj1467  29400  bnj1518  29410
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421
  Copyright terms: Public domain W3C validator