Theorem nfcrd 2917

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

Step	Hyp	Ref	Expression
1		nfcrd.1	. 2 ⊢ (𝜑 → Ⅎ𝑥𝐴)
2		nfcr 2913	. 2 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴)
3	1, 2	syl 18	1 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴)

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816   ∈ wcel 2145  Ⅎwnfc 2908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-clel 2836  df-nfc 2910

This theorem is used by:  nfeld  2934  dvelimdc  2947  nfraldw  3308  nfcsbd  3872  nfcsbw  3873  nfifd  4512  nfdisjw  5082  axextnd  10676  axrepndlem1  10677  axunndlem1  10680  axregnd  10689  nfchnd  18785  axsepg3  35809  axsepg3ALT  35810  axsepg5  35812  axextdist  36561  nfintd  50780  nfiund  50781  nfiundg  50782