![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfcvf2 | 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 2371. See nfcv 2903 for a version that replaces the distinctor with a disjoint variable condition, requiring fewer axioms. (Contributed by Mario Carneiro, 5-Dec-2016.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nfcvf2 | ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcvf 2932 | . 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦𝑥) | |
2 | 1 | naecoms 2428 | 1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1539 Ⅎwnfc 2883 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-13 2371 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-nf 1786 df-nfc 2885 |
This theorem is referenced by: dfid3 5577 oprabid 7440 axrepndlem1 10586 axrepndlem2 10587 axrepnd 10588 axunnd 10590 axpowndlem3 10593 axpowndlem4 10594 axpownd 10595 axregndlem2 10597 axinfndlem1 10599 axinfnd 10600 axacndlem4 10604 axacndlem5 10605 axacnd 10606 bj-nfcsym 35774 |
Copyright terms: Public domain | W3C validator |