This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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