Metamath Proof Explorer


Theorem elrn3

Description: Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017)

Ref Expression
Assertion elrn3
|- ( A e. ran B <-> ( B i^i ( _V X. { A } ) ) =/= (/) )

Proof

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