Theorem nfcrd 2902

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

Syntax hints:   → wi 4  Ⅎwnf 1781   ∈ wcel 2108  Ⅎwnfc 2893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782  df-clel 2819  df-nfc 2895

This theorem is referenced by:  nfeld  2920  dvelimdc  2936  nfraldw  3315  nfcsbd  3947  nfcsbw  3948  nfifd  4577  axextnd  10660  axrepndlem1  10661  axunndlem1  10664  axregnd  10673  axsepg2  35058  axsepg2ALT  35059  axextdist  35763  nfintd  48765  nfiund  48766  nfiundg  48767