|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > nfae | Structured version Visualization version GIF version | ||
| Description: All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2376. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) | 
| Ref | Expression | 
|---|---|
| nfae | ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | hbae 2435 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | |
| 2 | 1 | nf5i 2145 | 1 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 | 
| Colors of variables: wff setvar class | 
| Syntax hints: ∀wal 1537 Ⅎwnf 1782 | 
| 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-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 | 
| This theorem is referenced by: nfnae 2438 axc16nfALT 2441 dral2 2442 drex2 2446 drnf2 2448 sbequ5 2469 2ax6elem 2474 sbco3 2517 axbnd 2706 axrepnd 10635 axunnd 10637 axpowndlem3 10640 axpownd 10642 axregndlem1 10643 axregnd 10645 axacndlem1 10648 axacndlem2 10649 axacndlem3 10650 axacndlem4 10651 axacndlem5 10652 axacnd 10653 | 
| Copyright terms: Public domain | W3C validator |