Theorem nfwe

Description: Bound-variable hypothesis builder for well-orderings. (Contributed by Stefan O'Rear, 20-Jan-2015) (Revised by Mario Carneiro, 14-Oct-2016)

	Ref	Expression
Hypotheses	nffr.r	|- F/_ x R
	nffr.a	|- F/_ x A
Assertion	nfwe	|- F/ x R We A

Proof

Step	Hyp	Ref	Expression
1		nffr.r	|- F/_ x R
2		nffr.a	|- F/_ x A
3		df-we	|- ( R We A <-> ( R Fr A /\ R Or A ) )
4	1 2	nffr	|- F/ x R Fr A
5	1 2	nfso	|- F/ x R Or A
6	4 5	nfan	|- F/ x ( R Fr A /\ R Or A )
7	3 6	nfxfr	|- F/ x R We A