| Intuitionistic Logic Explorer | 
      
      
      < Previous  
      Next >
      
       Nearby theorems  | 
  ||
| Mirrors > Home > ILE Home > Th. List > nfraldxy | GIF version | ||
| Description: Old name for nfraldw 2529. (Contributed by Jim Kingdon, 29-May-2018.) (New usage is discouraged.) | 
| Ref | Expression | 
|---|---|
| nfraldxy.2 | ⊢ Ⅎ𝑦𝜑 | 
| nfraldxy.3 | ⊢ (𝜑 → Ⅎ𝑥𝐴) | 
| nfraldxy.4 | ⊢ (𝜑 → Ⅎ𝑥𝜓) | 
| Ref | Expression | 
|---|---|
| nfraldxy | ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | df-ral 2480 | . 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) | |
| 2 | nfraldxy.2 | . . 3 ⊢ Ⅎ𝑦𝜑 | |
| 3 | nfcv 2339 | . . . . . 6 ⊢ Ⅎ𝑥𝑦 | |
| 4 | 3 | a1i 9 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝑦) | 
| 5 | nfraldxy.3 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐴) | |
| 6 | 4, 5 | nfeld 2355 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) | 
| 7 | nfraldxy.4 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
| 8 | 6, 7 | nfimd 1599 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 ∈ 𝐴 → 𝜓)) | 
| 9 | 2, 8 | nfald 1774 | . 2 ⊢ (𝜑 → Ⅎ𝑥∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) | 
| 10 | 1, 9 | nfxfrd 1489 | 1 ⊢ (𝜑 → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜓) | 
| Colors of variables: wff set class | 
| Syntax hints: → wi 4 ∀wal 1362 Ⅎwnf 1474 ∈ wcel 2167 Ⅎwnfc 2326 ∀wral 2475 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-4 1524 ax-17 1540 ax-ial 1548 ax-i5r 1549 ax-ext 2178 | 
| This theorem depends on definitions: df-bi 117 df-nf 1475 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ral 2480 | 
| This theorem is referenced by: nfraldya 2532 nfralxy 2535 strcollnft 15630 | 
| Copyright terms: Public domain | W3C validator |