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 |