Metamath Proof Explorer

Theorem cnvimadfsn

Description: The support of functions "defined" by inverse images expressed by binary relations. (Contributed by AV, 7-Apr-2019)

Ref Expression
Assertion cnvimadfsn ⊢ R -1 V ∖ Z = x | ∃ y x R y ∧ y ≠ Z

Proof

Step Hyp Ref Expression
1 dfima3 ⊢ R -1 V ∖ Z = x | ∃ y y ∈ V ∖ Z ∧ y x ∈ R -1
2 eldifvsn ⊢ y ∈ V → y ∈ V ∖ Z ↔ y ≠ Z
3 2 elv ⊢ y ∈ V ∖ Z ↔ y ≠ Z
4 vex ⊢ y ∈ V
5 vex ⊢ x ∈ V
6 4 5 opelcnv ⊢ y x ∈ R -1 ↔ x y ∈ R
7 df-br ⊢ x R y ↔ x y ∈ R
8 6 7 bitr4i ⊢ y x ∈ R -1 ↔ x R y
9 3 8 anbi12ci ⊢ y ∈ V ∖ Z ∧ y x ∈ R -1 ↔ x R y ∧ y ≠ Z
10 9 exbii ⊢ ∃ y y ∈ V ∖ Z ∧ y x ∈ R -1 ↔ ∃ y x R y ∧ y ≠ Z
11 10 abbii ⊢ x | ∃ y y ∈ V ∖ Z ∧ y x ∈ R -1 = x | ∃ y x R y ∧ y ≠ Z
12 1 11 eqtri ⊢ R -1 V ∖ Z = x | ∃ y x R y ∧ y ≠ Z