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