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 ⊢ A ∈ ran ⁡ B ↔ B ∩ V × A ≠ ∅

Proof

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