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

Theorem nfcrd 2898
Description: Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfcrd.1 (𝜑𝑥𝐴)
Assertion
Ref Expression
nfcrd (𝜑 → Ⅎ𝑥 𝑦𝐴)
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem nfcrd
StepHypRef Expression
1 nfcrd.1 . 2 (𝜑𝑥𝐴)
2 nfcr 2894 . 2 (𝑥𝐴 → Ⅎ𝑥 𝑦𝐴)
31, 2syl 17 1 (𝜑 → Ⅎ𝑥 𝑦𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1782  wcel 2107  wnfc 2889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-nf 1783  df-clel 2815  df-nfc 2891
This theorem is referenced by:  nfeld  2916  dvelimdc  2929  nfraldw  3308  nfcsbd  3923  nfcsbw  3924  nfifd  4554  axextnd  10632  axrepndlem1  10633  axunndlem1  10636  axregnd  10645  axsepg2  35097  axsepg2ALT  35098  axextdist  35801  nfintd  49247  nfiund  49248  nfiundg  49249
  Copyright terms: Public domain W3C validator