| 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 } ) ) =/= (/) ) |