This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ 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 × { 𝐴 } ) ) ≠ ∅ )