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

Theorem nfcri 2386
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2384, 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 2385 . 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 2379
This theorem is referenced by:  nfnfc  2398  nfeq  2399  nfel  2400  cleqf  2416  sbabel  2418  r2alf  2551  r2exf  2552  nfrab  2694  cbvralf  2728  cbvrab  2755  nfccdeq  2950  sbcabel  3029  cbvcsb  3046  cbvralcsf  3104  cbvreucsf  3106  cbvrabcsf  3107  dfss2f  3132  nfdif  3258  nfun  3292  nfin  3336  nfiun  3891  nfiin  3892  cbviun  3899  cbviin  3900  cbvdisj  3963  nfdisj  3965  nfmpt  4068  tfis  4603  nfxp  4689  opeliunxp  4714  iunxpf  4806  nfmpt2  5836  cbvmpt2x  5844  nfsum  12115  cbvsum  12119  ptbasfi  17224  nfitg  19077  limciun  19192  nfprod1  24663  nfprod  24664  bnj1385  27898  bnj1476  27912  bnj900  27994  bnj1014  28025  bnj1123  28049  bnj1228  28074  bnj1321  28090  bnj1384  28095  bnj1398  28097  bnj1408  28099  bnj1444  28106  bnj1445  28107  bnj1446  28108  bnj1449  28111  bnj1467  28117  bnj1518  28127
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 1927  ax-ext 2237
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 1884  df-cleq 2249  df-clel 2252  df-nfc 2381
  Copyright terms: Public domain W3C validator