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

Theorem nfcri 2379
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2377, 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 2378 . 2  |-  ( y  e.  A  ->  A. x  y  e.  A )
32nfi 1556 1  |-  F/ x  y  e.  A
Colors of variables: wff set class
Syntax hints:   F/wnf 1539    e. wcel 1621   F/_wnfc 2372
This theorem is referenced by:  nfnfc  2391  nfeq  2392  nfel  2393  cleqf  2409  sbabel  2411  r2alf  2540  r2exf  2541  nfrab  2680  cbvralf  2703  cbvrab  2725  nfccdeq  2919  sbcabel  2998  cbvcsb  3013  cbvralcsf  3071  cbvreucsf  3073  cbvrabcsf  3074  dfss2f  3094  nfdif  3214  nfun  3241  nfin  3282  nfiun  3829  nfiin  3830  cbviun  3837  cbviin  3838  cbvdisj  3900  nfdisj  3902  nfmpt  4005  tfis  4536  nfxp  4622  opeliunxp  4647  iunxpf  4739  nfmpt2  5768  cbvmpt2x  5776  nfsum  12041  cbvsum  12045  ptbasfi  17108  nfitg  18961  limciun  19076  nfprod1  24476  nfprod  24477  bnj1385  27554  bnj1476  27568  bnj900  27650  bnj1014  27681  bnj1123  27705  bnj1228  27730  bnj1321  27746  bnj1384  27751  bnj1398  27753  bnj1408  27755  bnj1444  27762  bnj1445  27763  bnj1446  27764  bnj1449  27767  bnj1467  27773  bnj1518  27783
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-cleq 2246  df-clel 2249  df-nfc 2374
  Copyright terms: Public domain W3C validator