![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfae | Structured version Visualization version Unicode version |
Description: All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfae |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbae 2160 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | nfi 1685 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1675 df-nf 1679 |
This theorem is referenced by: nfnae 2163 axc16nfALT 2168 dral2 2169 drnf2 2175 sbequ5 2227 sbco3 2257 2ax6elem 2289 sbal 2302 exists1 2401 axi12 2440 axrepnd 9045 axunnd 9047 axpowndlem3 9050 axpownd 9052 axregndlem1 9053 axregnd 9055 axacndlem1 9058 axacndlem2 9059 axacndlem3 9060 axacndlem4 9061 axacndlem5 9062 axacnd 9063 |
Copyright terms: Public domain | W3C validator |