Theorem cnvresima

Description: An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009)

	Ref	Expression
Assertion	cnvresima	⊢ ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝐵 ) = ( ( ◡ 𝐹 “ 𝐵 ) ∩ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		19.41v	⊢ ( ∃ 𝑠 ( ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ) ∧ 𝑡 ∈ 𝐴 ) ↔ ( ∃ 𝑠 ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ) ∧ 𝑡 ∈ 𝐴 ) )
2		vex	⊢ 𝑠 ∈ V
3	2	opelresi	⊢ ( ⟨ 𝑡 , 𝑠 ⟩ ∈ ( 𝐹 ↾ 𝐴 ) ↔ ( 𝑡 ∈ 𝐴 ∧ ⟨ 𝑡 , 𝑠 ⟩ ∈ 𝐹 ) )
4		vex	⊢ 𝑡 ∈ V
5	2 4	opelcnv	⊢ ( ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ↔ ⟨ 𝑡 , 𝑠 ⟩ ∈ ( 𝐹 ↾ 𝐴 ) )
6	2 4	opelcnv	⊢ ( ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ↔ ⟨ 𝑡 , 𝑠 ⟩ ∈ 𝐹 )
7	6	anbi2ci	⊢ ( ( ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ∧ 𝑡 ∈ 𝐴 ) ↔ ( 𝑡 ∈ 𝐴 ∧ ⟨ 𝑡 , 𝑠 ⟩ ∈ 𝐹 ) )
8	3 5 7	3bitr4i	⊢ ( ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ↔ ( ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ∧ 𝑡 ∈ 𝐴 ) )
9	8	bianass	⊢ ( ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ) ↔ ( ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ) ∧ 𝑡 ∈ 𝐴 ) )
10	9	exbii	⊢ ( ∃ 𝑠 ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ) ↔ ∃ 𝑠 ( ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ) ∧ 𝑡 ∈ 𝐴 ) )
11	4	elima3	⊢ ( 𝑡 ∈ ( ◡ 𝐹 “ 𝐵 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ) )
12	11	anbi1i	⊢ ( ( 𝑡 ∈ ( ◡ 𝐹 “ 𝐵 ) ∧ 𝑡 ∈ 𝐴 ) ↔ ( ∃ 𝑠 ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ 𝐹 ) ∧ 𝑡 ∈ 𝐴 ) )
13	1 10 12	3bitr4i	⊢ ( ∃ 𝑠 ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ) ↔ ( 𝑡 ∈ ( ◡ 𝐹 “ 𝐵 ) ∧ 𝑡 ∈ 𝐴 ) )
14	4	elima3	⊢ ( 𝑡 ∈ ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝐵 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝐵 ∧ ⟨ 𝑠 , 𝑡 ⟩ ∈ ◡ ( 𝐹 ↾ 𝐴 ) ) )
15		elin	⊢ ( 𝑡 ∈ ( ( ◡ 𝐹 “ 𝐵 ) ∩ 𝐴 ) ↔ ( 𝑡 ∈ ( ◡ 𝐹 “ 𝐵 ) ∧ 𝑡 ∈ 𝐴 ) )
16	13 14 15	3bitr4i	⊢ ( 𝑡 ∈ ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝐵 ) ↔ 𝑡 ∈ ( ( ◡ 𝐹 “ 𝐵 ) ∩ 𝐴 ) )
17	16	eqriv	⊢ ( ◡ ( 𝐹 ↾ 𝐴 ) “ 𝐵 ) = ( ( ◡ 𝐹 “ 𝐵 ) ∩ 𝐴 )