Theorem nfcrd 2920

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149

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

This theorem is used by:  nfeld  2937  dvelimdc  2950  nfraldw  3311  nfcsbd  3876  nfcsbw  3877  nfifd  4515  nfdisjw  5087  axextnd  10715  axrepndlem1  10716  axunndlem1  10719  axregnd  10728  nfchnd  18835  axsepg3  35950  axsepg3ALT  35951  axsepg5  35953  axextdist  36776  nfintd  51187  nfiund  51188  nfiundg  51189