NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nfcri GIF version

Theorem nfcri 2483
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2481, this does not require y and A to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfcri.1 xA
Assertion
Ref Expression
nfcri x y A
Distinct variable group:   x,y
Allowed substitution hints:   A(x,y)

Proof of Theorem nfcri
StepHypRef Expression
1 nfcri.1 . . 3 xA
21nfcrii 2482 . 2 (y Ax y A)
32nfi 1551 1 x y A
Colors of variables: wff setvar class
Syntax hints:  wnf 1544   wcel 1710  wnfc 2476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-cleq 2346  df-clel 2349  df-nfc 2478
This theorem is referenced by:  nfnfc  2495  nfeq  2496  nfel  2497  cleqf  2513  sbabel  2515  r2alf  2649  r2exf  2650  nfrab  2792  cbvralf  2829  cbvrab  2857  sbcabel  3123  cbvcsb  3140  cbvralcsf  3198  cbvreucsf  3200  cbvrabcsf  3201  dfss2f  3264  nfiun  3995  nfiin  3996  cbviun  4003  cbviin  4004  nfxp  4810  opeliunxp  4820  nfmpt  5671  nfmpt2  5675  cbvmpt2x  5678  fmpt2x  5730
  Copyright terms: Public domain W3C validator