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

Theorem nfcri 2976
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2971, 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 2975 . 2 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
32nf5i 2143 1 𝑥 𝑦𝐴
Colors of variables: wff setvar class
Syntax hints:  wnf 1777  wcel 2107  wnfc 2966
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-10 2138  ax-11 2153  ax-12 2169
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-nf 1778  df-sb 2063  df-clel 2898  df-nfc 2968
This theorem is referenced by:  clelsb3fw  2986  clelsb3f  2987  clelsb3fOLD  2988  sbabel  3020  r2alf  3227  nfrabw  3391  nfrab  3392  cbvralfw  3443  cbvralf  3445  cbvrabw  3495  cbvrab  3496  rmo3f  3729  sbcabel  3865  cbvcsbw  3897  cbvcsb  3898  cbvrabcsfw  3928  cbvralcsf  3929  cbvreucsf  3931  cbvrabcsf  3932  nfdif  4106  nfun  4145  nfin  4197  nfiun  4946  nfiin  4947  nfiung  4948  nfiing  4949  cbviun  4958  cbviin  4959  cbviung  4960  cbviing  4961  cbvdisj  5038  nfdisjw  5040  nfdisj  5041  nfmpt  5160  cbvmptf  5162  cbvmptfg  5163  reusv2lem4  5298  nfxp  5587  opeliunxp  5618  iunxpf  5718  elrnmpt1  5829  nfmpo  7230  cbvmpox  7241  tfis  7562  fmpox  7761  nfsum1  15041  nfsumw  15042  nfsum  15043  fsum2dlem  15120  fsumcom2  15124  nfcprod  15260  cbvprod  15264  fprod2dlem  15329  fprodcom2  15333  gsum2d2lem  19029  dprd2d2  19102  ptbasfi  22124  restmetu  23114  ovoliunnul  24042  iundisj  24083  iunmbl2  24092  nfitg  24309  limciun  24426  reuxfrdf  30188  abrexss  30205  cbviunf  30241  iunin1f  30243  cbvdisjf  30255  disjabrex  30266  disjabrexf  30267  iundisjf  30273  ssrelf  30300  fmptcof2  30336  acunirnmpt2f  30340  iundisjfi  30451  locfinreflem  31009  esum2dlem  31256  oms0  31460  bnj1385  32009  bnj900  32106  bnj1014  32137  bnj1123  32161  bnj1228  32186  bnj1321  32202  bnj1384  32207  bnj1398  32209  bnj1408  32211  bnj1444  32218  bnj1445  32219  bnj1446  32220  bnj1449  32223  bnj1467  32229  bnj1518  32239  bj-nfcf  34145  mptsnunlem  34507  phpreu  34762  poimirlem26  34804  mbfposadd  34825  mpobi123f  35327  rababg  39817  ss2iundf  39888  binomcxplemnotnn0  40572  refsumcn  41171  iunssf  41236  cbvmpo2  41247  cbvmpo1  41248  iinssiin  41279  iinssf  41291  disjrnmpt2  41333  supxrleubrnmptf  41611  limcperiod  41793  limsupequzmptf  41896  dvnprodlem1  42115  stoweidlem16  42186  stoweidlem27  42197  stoweidlem28  42198  stoweidlem29  42199  stoweidlem31  42201  stoweidlem34  42204  stoweidlem35  42205  stoweidlem57  42227  stoweidlem59  42229  stirlinglem5  42248  fourierdlem16  42293  fourierdlem21  42298  fourierdlem22  42299  fourierdlem31  42308  fourierdlem48  42324  fourierdlem51  42327  fourierdlem53  42329  fourierdlem80  42356  fourierdlem93  42369  etransclem32  42436  opeliun2xp  44283  cbvmpox2  44286
  Copyright terms: Public domain W3C validator