![]() |
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 2379. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nfae | ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbae 2442 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | |
2 | 1 | nf5i 2147 | 1 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ∀wal 1536 Ⅎ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 1911 ax-6 1970 ax-7 2015 ax-10 2142 ax-11 2158 ax-12 2175 ax-13 2379 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-nf 1786 |
This theorem is referenced by: nfnae 2445 axc16nfALT 2448 dral2 2449 drex2 2453 drnf2 2455 sbequ5 2477 2ax6elem 2482 sbco3 2532 sbalOLD 2551 axbnd 2769 axrepnd 10005 axunnd 10007 axpowndlem3 10010 axpownd 10012 axregndlem1 10013 axregnd 10015 axacndlem1 10018 axacndlem2 10019 axacndlem3 10020 axacndlem4 10021 axacndlem5 10022 axacnd 10023 |
Copyright terms: Public domain | W3C validator |