nfa1 - Metamath Proof Explorer

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

Theorem nfa1 1833

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 1832	. 2
2	1	nfi 1597	1

Colors of variables: wff setvar class

Syntax hints:

wal 1368

wnf 1590

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-12 1794

This theorem depends on definitions: df-bi 185 df-ex 1588 df-nf 1591

This theorem is referenced by: axc4i 1834 nfnf1 1835 nfna1 1839 ax16nf 1879 19.12 1885 nfa2 1888 nfia1 1889 nf2 1897 equs5a 1915 equs5e 1916 cbv1h 1971 dral1 2024 nfald2 2030 ax12v2 2040 equs5 2049 axc14 2070 sbf2 2080 nfsb4t 2087 sbcom3 2112 sbco3 2121 sb56 2139 sbal1OLD 2179 exsb 2188 nfeu1 2273 mo3OLD 2306 eupickbiOLD 2354 moexex 2356 moexexOLD 2357 2eu1OLD 2372 2eu4OLD 2376 2eu6 2378 exists2 2384 nfaba1 2618 nfra1 2877 ceqsalgALT 3096 elrab3t 3215 csbie2t 3416 sbcnestgf 3791 dfnfc2 4209 mpteq12f 4468 axrep2 4505 axrep3 4506 axrep4 4507 alxfr 4605 copsex2t 4678 mosubopt 4689 fv3 5804 fvmptt 5890 fnoprabg 6293 pssnn 7634 fiint 7691 aceq1 8390 zorn2lem4 8771 axpowndlem3 8867 axpowndlem3OLD 8868 zfcndrep 8884 mreexexd 14690 dfon2lem7 27738 wl-nfimf1 28494 wl-nfae1 28496 wl-sb8t 28516 wl-sbnf1 28519 wl-lem-moexsb 28533 wl-mo2t 28536 wl-mo3t 28537 wl-sb8eut 28538 wl-ax11-lem3 28543 wl-sbcom3 28551 sbali 29058 sbcalf 29060 nfbii2 29111 setindtr 29513 axc11next 29800 iotain 29811 pm14.122b 29817 pm14.123b 29820 eubi 29830 rexsb 30132 ax6e2ndeqVD 31947 e2ebindALT 31967 ax6e2ndeqALT 31969 bj-alalbial 32493 bj-exalbial 32494 bj-biexal1 32497 bj-bialal 32500 bj-cbv1hv 32531 bj-ax16nf 32561 bj-dral1v 32563 bj-axc15v 32567 bj-equs5v 32569 bj-sb56 32586 bj-axrep2 32612 bj-axrep3 32613 bj-axrep4 32614 ax11-pm 32642 bj-snsetex 32758