Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfcvf | Structured version Visualization version GIF version |
Description: If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. (Contributed by Mario Carneiro, 8-Oct-2016.) |
Ref | Expression |
---|---|
nfcvf | ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2751 | . 2 ⊢ Ⅎ𝑥𝑧 | |
2 | nfcv 2751 | . 2 ⊢ Ⅎ𝑧𝑦 | |
3 | id 22 | . 2 ⊢ (𝑧 = 𝑦 → 𝑧 = 𝑦) | |
4 | 1, 2, 3 | dvelimc 2773 | 1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1473 Ⅎwnfc 2738 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-cleq 2603 df-clel 2606 df-nfc 2740 |
This theorem is referenced by: nfcvf2 2775 nfrald 2928 ralcom2 3083 nfreud 3091 nfrmod 3092 nfrmo 3094 nfdisj 4565 nfcvb 4824 nfiotad 5771 nfriotad 6519 nfixp 7813 axextnd 9292 axrepndlem2 9294 axrepnd 9295 axunndlem1 9296 axunnd 9297 axpowndlem2 9299 axpowndlem4 9301 axregndlem2 9304 axregnd 9305 axinfndlem1 9306 axinfnd 9307 axacndlem4 9311 axacndlem5 9312 axacnd 9313 axextdist 30949 bj-nfcsym 32079 |
Copyright terms: Public domain | W3C validator |