ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfcri GIF version

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

Proof of Theorem nfcri
StepHypRef Expression
1 nfcri.1 . . 3 𝑥𝐴
21nfcrii 2187 . 2 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
32nfi 1367 1 𝑥 𝑦𝐴
Colors of variables: wff set class
Syntax hints:  wnf 1365  wcel 1409  wnfc 2181
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-cleq 2049  df-clel 2052  df-nfc 2183
This theorem is referenced by:  nfnfc  2200  nfeq  2201  nfel  2202  cleqf  2217  sbabel  2219  r2alf  2358  r2exf  2359  nfrabxy  2507  cbvralf  2544  cbvrexf  2545  cbvrab  2572  nfccdeq  2785  sbcabel  2867  cbvcsb  2884  cbvralcsf  2936  cbvrexcsf  2937  cbvreucsf  2938  cbvrabcsf  2939  dfss2f  2964  nfdif  3093  nfun  3127  nfin  3171  nfop  3593  nfiunxy  3711  nfiinxy  3712  nfiunya  3713  nfiinya  3714  cbviun  3722  cbviin  3723  cbvdisj  3783  nfdisjv  3785  nfmpt  3877  nffrfor  4113  onintrab2im  4272  tfis  4334  nfxp  4399  opeliunxp  4423  iunxpf  4512  elrnmpt1  4613  fvmptssdm  5283  nfmpt2  5601  cbvmpt2x  5610  fmpt2x  5854  nffrec  6013  nfsum1  10106  nfsum  10107
  Copyright terms: Public domain W3C validator