![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfcrd | Structured version Visualization version GIF version |
Description: Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfcrd.1 | ⊢ (𝜑 → Ⅎ𝑥𝐴) |
Ref | Expression |
---|---|
nfcrd | ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcrd.1 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝐴) | |
2 | nfcr 2893 | . 2 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Ⅎwnf 1780 ∈ wcel 2106 Ⅎwnfc 2888 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-nf 1781 df-clel 2814 df-nfc 2890 |
This theorem is referenced by: nfeld 2915 dvelimdc 2928 nfraldw 3307 nfcsbd 3934 nfcsbw 3935 nfifd 4560 axextnd 10629 axrepndlem1 10630 axunndlem1 10633 axregnd 10642 axsepg2 35075 axsepg2ALT 35076 axextdist 35781 nfintd 48904 nfiund 48905 nfiundg 48906 |
Copyright terms: Public domain | W3C validator |