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 2373. See nfcv 2908 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 2710. (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 2454 | . 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 ∈ 𝑦) |
5 | 1, 4 | nfcd 2896 | 1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1537 Ⅎwnfc 2888 |
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 2373 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-ex 1783 df-nf 1787 df-nfc 2890 |
This theorem is referenced by: nfcvf2 2938 nfrald 3151 ralcom2 3291 nfreud 3303 nfrmod 3304 nfrmo 3310 nfdisj 5053 nfcvb 5300 nfriotad 7253 nfixp 8714 axextnd 10356 axrepndlem2 10358 axrepnd 10359 axunndlem1 10360 axunnd 10361 axpowndlem2 10363 axpowndlem4 10365 axregndlem2 10368 axregnd 10369 axinfndlem1 10370 axinfnd 10371 axacndlem4 10375 axacndlem5 10376 axacnd 10377 axextdist 33784 bj-nfcsym 35093 |
Copyright terms: Public domain | W3C validator |