Theorem nffr

Description: Bound-variable hypothesis builder for well-founded relations. (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	nffr	|- F/ x R Fr A

Proof

Step	Hyp	Ref	Expression
1		nffr.r	|- F/_ x R
2		nffr.a	|- F/_ x A
3		df-fr	|- ( R Fr A <-> A. a ( ( a C_ A /\ a =/= (/) ) -> E. b e. a A. c e. a -. c R b ) )
4		nfcv	|- F/_ x a
5	4 2	nfss	|- F/ x a C_ A
6		nfv	|- F/ x a =/= (/)
7	5 6	nfan	|- F/ x ( a C_ A /\ a =/= (/) )
8		nfcv	|- F/_ x c
9		nfcv	|- F/_ x b
10	8 1 9	nfbr	|- F/ x c R b
11	10	nfn	|- F/ x -. c R b
12	4 11	nfralw	|- F/ x A. c e. a -. c R b
13	4 12	nfrexw	|- F/ x E. b e. a A. c e. a -. c R b
14	7 13	nfim	|- F/ x ( ( a C_ A /\ a =/= (/) ) -> E. b e. a A. c e. a -. c R b )
15	14	nfal	|- F/ x A. a ( ( a C_ A /\ a =/= (/) ) -> E. b e. a A. c e. a -. c R b )
16	3 15	nfxfr	|- F/ x R Fr A