|   | 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 2376. See nfcv 2904 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 2707. (Revised by Wolf Lammen, 10-May-2023.) (New usage is discouraged.) | 
| Ref | Expression | 
|---|---|
| nfcvf | ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | nfv 1913 | . 2 ⊢ Ⅎ𝑤 ¬ ∀𝑥 𝑥 = 𝑦 | |
| 2 | nfv 1913 | . . 3 ⊢ Ⅎ𝑥 𝑤 ∈ 𝑧 | |
| 3 | elequ2 2122 | . . 3 ⊢ (𝑧 = 𝑦 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑦)) | |
| 4 | 2, 3 | dvelimnf 2457 | . 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 ∈ 𝑦) | 
| 5 | 1, 4 | nfcd 2897 | 1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ∀wal 1537 Ⅎwnfc 2889 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-13 2376 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-ex 1779 df-nf 1783 df-nfc 2891 | 
| This theorem is referenced by: nfcvf2 2932 nfrald 3371 ralcom2 3376 nfrmod 3431 nfreud 3432 nfrmo 3433 nfdisj 5122 nfcvb 5375 nfriotad 7400 nfixp 8958 axextnd 10632 axrepndlem2 10634 axrepnd 10635 axunndlem1 10636 axunnd 10637 axpowndlem2 10639 axpowndlem4 10641 axregndlem2 10644 axregnd 10645 axinfndlem1 10646 axinfnd 10647 axacndlem4 10651 axacndlem5 10652 axacnd 10653 axsepg2 35097 axsepg2ALT 35098 axnulg 35107 axextdist 35801 bj-nfcsym 36901 | 
| Copyright terms: Public domain | W3C validator |