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

Theorem nfcri 2413
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2411, 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 2412 . 2  |-  ( y  e.  A  ->  A. x  y  e.  A )
32nfi 1538 1  |-  F/ x  y  e.  A
Colors of variables: wff set class
Syntax hints:   F/wnf 1531    e. wcel 1684   F/_wnfc 2406
This theorem is referenced by:  nfnfc  2425  nfeq  2426  nfel  2427  cleqf  2443  sbabel  2445  r2alf  2578  r2exf  2579  nfrab  2721  cbvralf  2758  cbvrab  2786  nfccdeq  2989  sbcabel  3068  cbvcsb  3085  cbvralcsf  3143  cbvreucsf  3145  cbvrabcsf  3146  dfss2f  3171  nfdif  3297  nfun  3331  nfin  3375  nfiun  3931  nfiin  3932  cbviun  3939  cbviin  3940  cbvdisj  4003  nfdisj  4005  nfmpt  4108  tfis  4645  nfxp  4715  opeliunxp  4740  iunxpf  4832  nfmpt2  5916  cbvmpt2x  5924  nfsum  12164  cbvsum  12168  ptbasfi  17276  nfitg  19129  limciun  19244  cbvdisjf  23350  disjabrex  23359  disjabrexf  23360  nfprod1  25310  nfprod  25311  bnj1385  28865  bnj1476  28879  bnj900  28961  bnj1014  28992  bnj1123  29016  bnj1228  29041  bnj1321  29057  bnj1384  29062  bnj1398  29064  bnj1408  29066  bnj1444  29073  bnj1445  29074  bnj1446  29075  bnj1449  29078  bnj1467  29084  bnj1518  29094
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408
  Copyright terms: Public domain W3C validator