nfre1 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > nfre1		Unicode version

Theorem nfre1 2670

Description:

is not free in

. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)

**Assertion**
Ref	Expression
nfre1

**Proof of Theorem nfre1**
Step	Hyp	Ref	Expression
1		df-rex 2620	. 2 $/\$
2		nfe1 1732	. 2 $/\$
3	1, 2	nfxfr 1570	1

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 358

wex 1541

wnf 1544

wcel 1710

wrex 2615

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-6 1729

This theorem depends on definitions: df-bi 177 df-ex 1542 df-nf 1545 df-rex 2620

This theorem is referenced by: 2rmorex 3040 nfiu1 3997 fun11iun 5305