|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > nfcii | Structured version Visualization version GIF version | ||
| Description: Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) | 
| Ref | Expression | 
|---|---|
| nfcii.1 | ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) | 
| Ref | Expression | 
|---|---|
| nfcii | ⊢ Ⅎ𝑥𝐴 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | nfcii.1 | . . 3 ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) | |
| 2 | 1 | nf5i 2145 | . 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 | 
| 3 | 2 | nfci 2892 | 1 ⊢ Ⅎ𝑥𝐴 | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∀wal 1537 ∈ wcel 2107 Ⅎ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-10 2140 | 
| This theorem depends on definitions: df-bi 207 df-ex 1779 df-nf 1783 df-nfc 2891 | 
| This theorem is referenced by: bnj1316 34835 bnj1385 34847 bnj1400 34850 bnj1468 34861 bnj1534 34868 bnj1542 34872 bnj1228 35026 bnj1307 35038 bnj1448 35062 bnj1466 35068 bnj1463 35070 bnj1491 35072 bnj1312 35073 bnj1498 35076 bnj1520 35081 bnj1525 35084 bnj1529 35085 bnj1523 35086 | 
| Copyright terms: Public domain | W3C validator |