![]() |
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 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2372. See nfcv 2904 for a version that replaces the distinctor with a disjoint variable condition, requiring fewer axioms. (Contributed by Mario Carneiro, 8-Oct-2016.) Avoid ax-ext 2704. (Revised by Wolf Lammen, 10-May-2023.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nfcvf | ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1918 | . 2 ⊢ Ⅎ𝑤 ¬ ∀𝑥 𝑥 = 𝑦 | |
2 | nfv 1918 | . . 3 ⊢ Ⅎ𝑥 𝑤 ∈ 𝑧 | |
3 | elequ2 2122 | . . 3 ⊢ (𝑧 = 𝑦 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑦)) | |
4 | 2, 3 | dvelimnf 2453 | . 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 ∈ 𝑦) |
5 | 1, 4 | nfcd 2892 | 1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1540 Ⅎwnfc 2884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-13 2372 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-nfc 2886 |
This theorem is referenced by: nfcvf2 2934 nfrald 3369 ralcom2 3374 nfrmod 3429 nfreud 3430 nfrmo 3431 nfdisj 5127 nfcvb 5375 nfriotad 7377 nfixp 8911 axextnd 10586 axrepndlem2 10588 axrepnd 10589 axunndlem1 10590 axunnd 10591 axpowndlem2 10593 axpowndlem4 10595 axregndlem2 10598 axregnd 10599 axinfndlem1 10600 axinfnd 10601 axacndlem4 10605 axacndlem5 10606 axacnd 10607 axextdist 34771 bj-nfcsym 35779 |
Copyright terms: Public domain | W3C validator |