Theorem elrn3

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

	Ref	Expression
Assertion	elrn3	⊢ ( 𝐴 ∈ ran 𝐵 ↔ ( 𝐵 ∩ ( V × { 𝐴 } ) ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-rn	⊢ ran 𝐵 = dom ◡ 𝐵
2	1	eleq2i	⊢ ( 𝐴 ∈ ran 𝐵 ↔ 𝐴 ∈ dom ◡ 𝐵 )
3		eldm3	⊢ ( 𝐴 ∈ dom ◡ 𝐵 ↔ ( ◡ 𝐵 ↾ { 𝐴 } ) ≠ ∅ )
4		cnvxp	⊢ ◡ ( V × { 𝐴 } ) = ( { 𝐴 } × V )
5	4	ineq2i	⊢ ( ◡ 𝐵 ∩ ◡ ( V × { 𝐴 } ) ) = ( ◡ 𝐵 ∩ ( { 𝐴 } × V ) )
6		cnvin	⊢ ◡ ( 𝐵 ∩ ( V × { 𝐴 } ) ) = ( ◡ 𝐵 ∩ ◡ ( V × { 𝐴 } ) )
7		df-res	⊢ ( ◡ 𝐵 ↾ { 𝐴 } ) = ( ◡ 𝐵 ∩ ( { 𝐴 } × V ) )
8	5 6 7	3eqtr4ri	⊢ ( ◡ 𝐵 ↾ { 𝐴 } ) = ◡ ( 𝐵 ∩ ( V × { 𝐴 } ) )
9	8	eqeq1i	⊢ ( ( ◡ 𝐵 ↾ { 𝐴 } ) = ∅ ↔ ◡ ( 𝐵 ∩ ( V × { 𝐴 } ) ) = ∅ )
10		relinxp	⊢ Rel ( 𝐵 ∩ ( V × { 𝐴 } ) )
11		cnveq0	⊢ ( Rel ( 𝐵 ∩ ( V × { 𝐴 } ) ) → ( ( 𝐵 ∩ ( V × { 𝐴 } ) ) = ∅ ↔ ◡ ( 𝐵 ∩ ( V × { 𝐴 } ) ) = ∅ ) )
12	10 11	ax-mp	⊢ ( ( 𝐵 ∩ ( V × { 𝐴 } ) ) = ∅ ↔ ◡ ( 𝐵 ∩ ( V × { 𝐴 } ) ) = ∅ )
13	9 12	bitr4i	⊢ ( ( ◡ 𝐵 ↾ { 𝐴 } ) = ∅ ↔ ( 𝐵 ∩ ( V × { 𝐴 } ) ) = ∅ )
14	13	necon3bii	⊢ ( ( ◡ 𝐵 ↾ { 𝐴 } ) ≠ ∅ ↔ ( 𝐵 ∩ ( V × { 𝐴 } ) ) ≠ ∅ )
15	2 3 14	3bitri	⊢ ( 𝐴 ∈ ran 𝐵 ↔ ( 𝐵 ∩ ( V × { 𝐴 } ) ) ≠ ∅ )