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 2384. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nfae | ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbae 2447 | . 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | |
2 | 1 | nf5i 2144 | 1 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ∀wal 1529 Ⅎwnf 1778 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-10 2139 ax-11 2154 ax-12 2170 ax-13 2384 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1534 df-ex 1775 df-nf 1779 |
This theorem is referenced by: nfnae 2450 axc16nfALT 2453 dral2 2454 drex2 2458 drnf2 2460 sbequ5 2482 2ax6elem 2487 sbco3 2549 sbalOLD 2569 axi12OLD 2788 axbnd 2789 axrepnd 10008 axunnd 10010 axpowndlem3 10013 axpownd 10015 axregndlem1 10016 axregnd 10018 axacndlem1 10021 axacndlem2 10022 axacndlem3 10023 axacndlem4 10024 axacndlem5 10025 axacnd 10026 |
Copyright terms: Public domain | W3C validator |