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

Theorem nfcri 2222
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2220, 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 2221 . 2 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
32nfi 1396 1 𝑥 𝑦𝐴
Colors of variables: wff set class
Syntax hints:  wnf 1394  wcel 1438  wnfc 2215
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-cleq 2081  df-clel 2084  df-nfc 2217
This theorem is referenced by:  clelsb3f  2232  nfnfc  2235  nfeq  2236  nfel  2237  cleqf  2252  sbabel  2254  r2alf  2395  r2exf  2396  nfrabxy  2547  cbvralf  2584  cbvrexf  2585  cbvrab  2617  rmo3f  2810  nfccdeq  2836  sbcabel  2918  cbvcsb  2935  cbvralcsf  2988  cbvrexcsf  2989  cbvreucsf  2990  cbvrabcsf  2991  dfss2f  3014  nfdif  3119  nfun  3154  nfin  3204  nfop  3633  nfiunxy  3751  nfiinxy  3752  nfiunya  3753  nfiinya  3754  cbviun  3762  cbviin  3763  iunxsngf  3802  cbvdisj  3824  nfdisjv  3826  disjiun  3832  nfmpt  3922  cbvmptf  3924  nffrfor  4166  onintrab2im  4325  tfis  4388  nfxp  4454  opeliunxp  4481  iunxpf  4572  elrnmpt1  4674  fvmptssdm  5371  nfmpt2  5699  cbvmpt2x  5708  fmpt2x  5952  nffrec  6143  nfsum1  10709  nfsum  10710  fsum2dlemstep  10791  fisumcom2  10795
  Copyright terms: Public domain W3C validator