![]() |
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 2372. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nfae | ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbae 2431 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | |
2 | 1 | nf5i 2143 | 1 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ∀wal 1540 Ⅎwnf 1786 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-10 2138 ax-11 2155 ax-12 2172 ax-13 2372 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 |
This theorem is referenced by: nfnae 2434 axc16nfALT 2437 dral2 2438 drex2 2442 drnf2 2444 sbequ5 2465 2ax6elem 2470 sbco3 2513 axbnd 2703 axrepnd 10589 axunnd 10591 axpowndlem3 10594 axpownd 10596 axregndlem1 10597 axregnd 10599 axacndlem1 10602 axacndlem2 10603 axacndlem3 10604 axacndlem4 10605 axacndlem5 10606 axacnd 10607 |
Copyright terms: Public domain | W3C validator |