Step |
Hyp |
Ref |
Expression |
1 |
|
df-rn |
|- ran B = dom `' B |
2 |
1
|
eleq2i |
|- ( A e. ran B <-> A e. dom `' B ) |
3 |
|
eldm3 |
|- ( A e. dom `' B <-> ( `' B |` { A } ) =/= (/) ) |
4 |
|
cnvxp |
|- `' ( _V X. { A } ) = ( { A } X. _V ) |
5 |
4
|
ineq2i |
|- ( `' B i^i `' ( _V X. { A } ) ) = ( `' B i^i ( { A } X. _V ) ) |
6 |
|
cnvin |
|- `' ( B i^i ( _V X. { A } ) ) = ( `' B i^i `' ( _V X. { A } ) ) |
7 |
|
df-res |
|- ( `' B |` { A } ) = ( `' B i^i ( { A } X. _V ) ) |
8 |
5 6 7
|
3eqtr4ri |
|- ( `' B |` { A } ) = `' ( B i^i ( _V X. { A } ) ) |
9 |
8
|
eqeq1i |
|- ( ( `' B |` { A } ) = (/) <-> `' ( B i^i ( _V X. { A } ) ) = (/) ) |
10 |
|
relinxp |
|- Rel ( B i^i ( _V X. { A } ) ) |
11 |
|
cnveq0 |
|- ( Rel ( B i^i ( _V X. { A } ) ) -> ( ( B i^i ( _V X. { A } ) ) = (/) <-> `' ( B i^i ( _V X. { A } ) ) = (/) ) ) |
12 |
10 11
|
ax-mp |
|- ( ( B i^i ( _V X. { A } ) ) = (/) <-> `' ( B i^i ( _V X. { A } ) ) = (/) ) |
13 |
9 12
|
bitr4i |
|- ( ( `' B |` { A } ) = (/) <-> ( B i^i ( _V X. { A } ) ) = (/) ) |
14 |
13
|
necon3bii |
|- ( ( `' B |` { A } ) =/= (/) <-> ( B i^i ( _V X. { A } ) ) =/= (/) ) |
15 |
2 3 14
|
3bitri |
|- ( A e. ran B <-> ( B i^i ( _V X. { A } ) ) =/= (/) ) |