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