![]() |
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 10585 axunnd 10587 axpowndlem3 10590 axpownd 10592 axregndlem1 10593 axregnd 10595 axacndlem1 10598 axacndlem2 10599 axacndlem3 10600 axacndlem4 10601 axacndlem5 10602 axacnd 10603 |
Copyright terms: Public domain | W3C validator |