|   | 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 2377. See nfcv 2905 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 2434 | 1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ∀wal 1538 Ⅎwnfc 2890 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-13 2377 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-nfc 2892 | 
| This theorem is referenced by: dfid3 5581 oprabid 7463 axrepndlem1 10632 axrepndlem2 10633 axrepnd 10634 axunnd 10636 axpowndlem3 10639 axpowndlem4 10640 axpownd 10641 axregndlem2 10643 axinfndlem1 10645 axinfnd 10646 axacndlem4 10650 axacndlem5 10651 axacnd 10652 bj-nfcsym 36900 | 
| Copyright terms: Public domain | W3C validator |