Step |
Hyp |
Ref |
Expression |
1 |
|
rnmptssbi.1 |
|- F/ x ph |
2 |
|
rnmptssbi.2 |
|- F = ( x e. A |-> B ) |
3 |
|
rnmptssbi.3 |
|- ( ( ph /\ x e. A ) -> B e. V ) |
4 |
|
nfmpt1 |
|- F/_ x ( x e. A |-> B ) |
5 |
2 4
|
nfcxfr |
|- F/_ x F |
6 |
5
|
nfrn |
|- F/_ x ran F |
7 |
|
nfcv |
|- F/_ x C |
8 |
6 7
|
nfss |
|- F/ x ran F C_ C |
9 |
1 8
|
nfan |
|- F/ x ( ph /\ ran F C_ C ) |
10 |
|
simplr |
|- ( ( ( ph /\ ran F C_ C ) /\ x e. A ) -> ran F C_ C ) |
11 |
|
simpr |
|- ( ( ( ph /\ ran F C_ C ) /\ x e. A ) -> x e. A ) |
12 |
3
|
adantlr |
|- ( ( ( ph /\ ran F C_ C ) /\ x e. A ) -> B e. V ) |
13 |
2 11 12
|
elrnmpt1d |
|- ( ( ( ph /\ ran F C_ C ) /\ x e. A ) -> B e. ran F ) |
14 |
10 13
|
sseldd |
|- ( ( ( ph /\ ran F C_ C ) /\ x e. A ) -> B e. C ) |
15 |
9 14
|
ralrimia |
|- ( ( ph /\ ran F C_ C ) -> A. x e. A B e. C ) |
16 |
2
|
rnmptss |
|- ( A. x e. A B e. C -> ran F C_ C ) |
17 |
16
|
adantl |
|- ( ( ph /\ A. x e. A B e. C ) -> ran F C_ C ) |
18 |
15 17
|
impbida |
|- ( ph -> ( ran F C_ C <-> A. x e. A B e. C ) ) |