![]() |
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 2366. See nfcv 2892 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 2922 | . 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦𝑥) | |
2 | 1 | naecoms 2423 | 1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∀wal 1532 Ⅎwnfc 2876 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-13 2366 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-ex 1775 df-nf 1779 df-nfc 2878 |
This theorem is referenced by: dfid3 5583 oprabid 7456 axrepndlem1 10635 axrepndlem2 10636 axrepnd 10637 axunnd 10639 axpowndlem3 10642 axpowndlem4 10643 axpownd 10644 axregndlem2 10646 axinfndlem1 10648 axinfnd 10649 axacndlem4 10653 axacndlem5 10654 axacnd 10655 bj-nfcsym 36605 |
Copyright terms: Public domain | W3C validator |