nfa1 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nfa1		Structured version Unicode version

Theorem nfa1 1840

Description:

is not free in

. (Contributed by Mario Carneiro, 11-Aug-2016.)

**Assertion**
Ref	Expression
nfa1

**Proof of Theorem nfa1**
Step	Hyp	Ref	Expression
1		hba1 1839	. 2
2	1	nfi 1601	1

Colors of variables: wff setvar class

Syntax hints:

wal 1372

wnf 1594

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-10 1781 ax-12 1798

This theorem depends on definitions: df-bi 185 df-ex 1592 df-nf 1595

This theorem is referenced by: axc4i 1841 nfnf1 1842 nfna1 1846 ax16nf 1886 19.12 1892 nfa2 1895 nfia1 1896 nf2 1904 equs5a 1922 equs5e 1923 cbv1h 1982 dral1 2035 nfald2 2041 ax12v2 2051 equs5 2060 axc14 2081 sbf2 2091 nfsb4t 2098 sbcom3 2123 sbco3 2132 sb56 2149 sbal1OLD 2189 exsb 2198 nfeu1 2283 mo3OLD 2316 eupickbiOLD 2364 moexex 2366 moexexOLD 2367 2eu1OLD 2382 2eu4OLD 2386 2eu6 2388 exists2 2394 nfaba1 2629 nfra1 2840 ceqsalgALT 3134 elrab3t 3255 csbie2t 3459 sbcnestgf 3834 dfnfc2 4258 mpteq12f 4518 axrep2 4555 axrep3 4556 axrep4 4557 alxfr 4655 copsex2t 4729 mosubopt 4740 fv3 5872 fvmptt 5958 fnoprabg 6380 pssnn 7730 fiint 7788 aceq1 8489 zorn2lem4 8870 axpowndlem3 8966 axpowndlem3OLD 8967 zfcndrep 8983 mreexexd 14894 dfon2lem7 28786 wl-nfimf1 29543 wl-nfae1 29545 wl-sb8t 29565 wl-sbnf1 29568 wl-lem-moexsb 29582 wl-mo2t 29585 wl-mo3t 29586 wl-sb8eut 29587 wl-ax11-lem3 29592 wl-sbcom3 29600 sbali 30107 sbcalf 30109 nfbii2 30160 setindtr 30561 axc11next 30848 iotain 30859 pm14.122b 30865 pm14.123b 30868 eubi 30878 rexsb 31597 ax6e2ndeqVD 32666 e2ebindALT 32686 ax6e2ndeqALT 32688 bj-alalbial 33214 bj-exalbial 33215 bj-biexal1 33218 bj-bialal 33221 bj-cbv1hv 33252 bj-ax16nf 33282 bj-dral1v 33284 bj-axc15v 33288 bj-equs5v 33290 bj-sb56 33307 bj-axrep2 33333 bj-axrep3 33334 bj-axrep4 33335 ax11-pm 33363 bj-snsetex 33479