Theorem nfcrd 2885

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

Syntax hints:   → wi 4  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-clel 2803  df-nfc 2878

This theorem is referenced by:  nfeld  2903  dvelimdc  2916  nfraldw  3283  nfcsbd  3887  nfcsbw  3888  nfifd  4518  axextnd  10544  axrepndlem1  10545  axunndlem1  10548  axregnd  10557  axsepg2  35072  axsepg2ALT  35073  axextdist  35787  nfintd  49659  nfiund  49660  nfiundg  49661