Theorem nfcrd 2916

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 2912	. 2 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴)
3	1, 2	syl 18	1 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴)

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

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 2835  df-nfc 2909

This theorem is used by:  nfeld  2933  dvelimdc  2946  nfraldw  3307  nfcsbd  3872  nfcsbw  3873  nfifd  4512  nfdisjw  5082  axextnd  10601  axrepndlem1  10602  axunndlem1  10605  axregnd  10614  nfchnd  18700  axsepg3  35668  axsepg3ALT  35669  axsepg5  35671  axextdist  36377  nfintd  50600  nfiund  50601  nfiundg  50602