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 2900 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 2711. (Revised by Wolf Lammen, 10-May-2023.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nfcvf | ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1921 | . 2 ⊢ Ⅎ𝑤 ¬ ∀𝑥 𝑥 = 𝑦 | |
2 | nfv 1921 | . . 3 ⊢ Ⅎ𝑥 𝑤 ∈ 𝑧 | |
3 | elequ2 2129 | . . 3 ⊢ (𝑧 = 𝑦 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑦)) | |
4 | 2, 3 | dvelimnf 2454 | . 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 ∈ 𝑦) |
5 | 1, 4 | nfcd 2888 | 1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1540 Ⅎwnfc 2880 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-13 2373 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-nf 1791 df-nfc 2882 |
This theorem is referenced by: nfcvf2 2930 nfrald 3138 ralcom2 3267 nfreud 3276 nfrmod 3277 nfrmo 3281 nfdisj 5009 nfcvb 5244 nfriotad 7142 nfixp 8530 axextnd 10094 axrepndlem2 10096 axrepnd 10097 axunndlem1 10098 axunnd 10099 axpowndlem2 10101 axpowndlem4 10103 axregndlem2 10106 axregnd 10107 axinfndlem1 10108 axinfnd 10109 axacndlem4 10113 axacndlem5 10114 axacnd 10115 axextdist 33352 bj-nfcsym 34731 |
Copyright terms: Public domain | W3C validator |