![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfa1 | Structured version Visualization version Unicode version |
Description: ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfa1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hba1 1989 |
. 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-12 1944 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1675 df-nf 1679 |
This theorem is referenced by: axc4i 1991 nfnf1 1992 nfna1 1996 axc16nf 2038 19.12 2044 nfa2 2047 nfia1 2048 nf2 2052 equs5a 2079 equs5e 2080 sb56 2092 cbv1h 2122 dral1 2170 nfald2 2176 ax12v2 2186 equs5 2193 axc14 2212 sbf2 2222 nfsb4t 2229 sbcom3 2251 exsb 2308 nfeu1 2320 moexex 2381 2eu6 2398 exists2 2402 nfaba1 2608 nfra1 2781 ceqsalgALT 3085 elrab3t 3207 csbie2t 3404 sbcnestgf 3796 dfnfc2 4230 mpteq12f 4493 axrep2 4531 axrep3 4532 axrep4 4533 alxfr 4627 copsex2t 4702 mosubopt 4713 fv3 5901 fvmptt 5988 fnoprabg 6424 pssnn 7816 fiint 7874 aceq1 8574 zorn2lem4 8955 zfcndrep 9065 mreexexd 15603 dfon2lem7 30484 bj-alalbial 31340 bj-exalbial 31341 bj-biexal1 31344 bj-bialal 31347 bj-cbv1hv 31376 bj-axc16nf 31401 bj-dral1v 31403 bj-axc15v 31407 bj-equs5v 31409 bj-axrep2 31449 bj-axrep3 31450 bj-axrep4 31451 ax11-pm 31479 bj-mo3OLD 31492 bj-snsetex 31602 exlimim 31789 exellim 31792 wl-nfimf1 31903 wl-nfae1 31905 wl-sb8t 31925 wl-sbnf1 31928 wl-lem-moexsb 31942 wl-mo2tf 31945 wl-eutf 31947 wl-mo2t 31949 wl-mo3t 31950 wl-sb8eut 31951 wl-ax12v3 31957 wl-ax11-lem3 31962 wl-sbcom3 31970 sbali 32395 nfbii2 32447 setindtr 35924 axc11next 36801 iotain 36812 pm14.122b 36818 pm14.123b 36821 eubi 36831 ax6e2ndeqVD 37346 e2ebindALT 37366 ax6e2ndeqALT 37368 rexsb 38627 |
Copyright terms: Public domain | W3C validator |