![]() |
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 2375. See nfcv 2903 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 2706. (Revised by Wolf Lammen, 10-May-2023.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nfcvf | ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1912 | . 2 ⊢ Ⅎ𝑤 ¬ ∀𝑥 𝑥 = 𝑦 | |
2 | nfv 1912 | . . 3 ⊢ Ⅎ𝑥 𝑤 ∈ 𝑧 | |
3 | elequ2 2121 | . . 3 ⊢ (𝑧 = 𝑦 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑦)) | |
4 | 2, 3 | dvelimnf 2456 | . 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 ∈ 𝑦) |
5 | 1, 4 | nfcd 2896 | 1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1535 Ⅎwnfc 2888 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-13 2375 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-ex 1777 df-nf 1781 df-nfc 2890 |
This theorem is referenced by: nfcvf2 2931 nfrald 3370 ralcom2 3375 nfrmod 3429 nfreud 3430 nfrmo 3431 nfdisj 5128 nfcvb 5382 nfriotad 7399 nfixp 8956 axextnd 10629 axrepndlem2 10631 axrepnd 10632 axunndlem1 10633 axunnd 10634 axpowndlem2 10636 axpowndlem4 10638 axregndlem2 10641 axregnd 10642 axinfndlem1 10643 axinfnd 10644 axacndlem4 10648 axacndlem5 10649 axacnd 10650 axsepg2 35075 axsepg2ALT 35076 axnulg 35085 axextdist 35781 bj-nfcsym 36882 |
Copyright terms: Public domain | W3C validator |