![]() |
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 2793 | . 2 ⊢ Ⅎ𝑥𝑧 | |
2 | nfcv 2793 | . 2 ⊢ Ⅎ𝑧𝑦 | |
3 | id 22 | . 2 ⊢ (𝑧 = 𝑦 → 𝑧 = 𝑦) | |
4 | 1, 2, 3 | dvelimc 2816 | 1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1521 Ⅎwnfc 2780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-cleq 2644 df-clel 2647 df-nfc 2782 |
This theorem is referenced by: nfcvf2 2818 nfrald 2973 ralcom2 3133 nfreud 3141 nfrmod 3142 nfrmo 3144 nfdisj 4664 nfcvb 4928 nfriotad 6659 nfixp 7969 axextnd 9451 axrepndlem2 9453 axrepnd 9454 axunndlem1 9455 axunnd 9456 axpowndlem2 9458 axpowndlem4 9460 axregndlem2 9463 axregnd 9464 axinfndlem1 9465 axinfnd 9466 axacndlem4 9470 axacndlem5 9471 axacnd 9472 axextdist 31829 bj-nfcsym 33011 |
Copyright terms: Public domain | W3C validator |