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