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 ( 𝑅 “ ( V ∖ { 𝑍 } ) ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) }

Proof

Step Hyp Ref Expression
1 dfima3 ( 𝑅 “ ( V ∖ { 𝑍 } ) ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) }
2 eldifvsn ( 𝑦 ∈ V → ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ↔ 𝑦𝑍 ) )
3 2 elv ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ↔ 𝑦𝑍 )
4 vex 𝑦 ∈ V
5 vex 𝑥 ∈ V
6 4 5 opelcnv ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
7 df-br ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
8 6 7 bitr4i ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅𝑥 𝑅 𝑦 )
9 3 8 anbi12ci ( ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) ↔ ( 𝑥 𝑅 𝑦𝑦𝑍 ) )
10 9 exbii ( ∃ 𝑦 ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) ↔ ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) )
11 10 abbii { 𝑥 ∣ ∃ 𝑦 ( 𝑦 ∈ ( V ∖ { 𝑍 } ) ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝑅 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) }
12 1 11 eqtri ( 𝑅 “ ( V ∖ { 𝑍 } ) ) = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 𝑅 𝑦𝑦𝑍 ) }