![]() |
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 2371. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nfae | ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbae 2430 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | |
2 | 1 | nf5i 2142 | 1 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ∀wal 1539 Ⅎwnf 1785 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-10 2137 ax-11 2154 ax-12 2171 ax-13 2371 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-nf 1786 |
This theorem is referenced by: nfnae 2433 axc16nfALT 2436 dral2 2437 drex2 2441 drnf2 2443 sbequ5 2464 2ax6elem 2469 sbco3 2512 axbnd 2702 axrepnd 10591 axunnd 10593 axpowndlem3 10596 axpownd 10598 axregndlem1 10599 axregnd 10601 axacndlem1 10604 axacndlem2 10605 axacndlem3 10606 axacndlem4 10607 axacndlem5 10608 axacnd 10609 |
Copyright terms: Public domain | W3C validator |