![]() |
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 2375. 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 2930 | . 2 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦𝑥) | |
2 | 1 | naecoms 2432 | 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: dfid3 5586 oprabid 7463 axrepndlem1 10630 axrepndlem2 10631 axrepnd 10632 axunnd 10634 axpowndlem3 10637 axpowndlem4 10638 axpownd 10639 axregndlem2 10641 axinfndlem1 10643 axinfnd 10644 axacndlem4 10648 axacndlem5 10649 axacnd 10650 bj-nfcsym 36882 |
Copyright terms: Public domain | W3C validator |