# Metamath Proof Explorer

## 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 ( ( 𝐹𝐴 ) “ 𝐵 ) = ( ( 𝐹𝐵 ) ∩ 𝐴 )