Metamath Proof Explorer


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 nfrex
 |-  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