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 ⊢ F ↾ A -1 B = F -1 B ∩ A

Proof

Step Hyp Ref Expression
1 19.41v ⊢ ∃ s s ∈ B ∧ s t ∈ F -1 ∧ t ∈ A ↔ ∃ s s ∈ B ∧ s t ∈ F -1 ∧ t ∈ A
2 vex ⊢ s ∈ V
3 2 opelresi ⊢ t s ∈ F ↾ A ↔ t ∈ A ∧ t s ∈ F
4 vex ⊢ t ∈ V
5 2 4 opelcnv ⊢ s t ∈ F ↾ A -1 ↔ t s ∈ F ↾ A
6 2 4 opelcnv ⊢ s t ∈ F -1 ↔ t s ∈ F
7 6 anbi2ci ⊢ s t ∈ F -1 ∧ t ∈ A ↔ t ∈ A ∧ t s ∈ F
8 3 5 7 3bitr4i ⊢ s t ∈ F ↾ A -1 ↔ s t ∈ F -1 ∧ t ∈ A
9 8 bianass ⊢ s ∈ B ∧ s t ∈ F ↾ A -1 ↔ s ∈ B ∧ s t ∈ F -1 ∧ t ∈ A
10 9 exbii ⊢ ∃ s s ∈ B ∧ s t ∈ F ↾ A -1 ↔ ∃ s s ∈ B ∧ s t ∈ F -1 ∧ t ∈ A
11 4 elima3 ⊢ t ∈ F -1 B ↔ ∃ s s ∈ B ∧ s t ∈ F -1
12 11 anbi1i ⊢ t ∈ F -1 B ∧ t ∈ A ↔ ∃ s s ∈ B ∧ s t ∈ F -1 ∧ t ∈ A
13 1 10 12 3bitr4i ⊢ ∃ s s ∈ B ∧ s t ∈ F ↾ A -1 ↔ t ∈ F -1 B ∧ t ∈ A
14 4 elima3 ⊢ t ∈ F ↾ A -1 B ↔ ∃ s s ∈ B ∧ s t ∈ F ↾ A -1
15 elin ⊢ t ∈ F -1 B ∩ A ↔ t ∈ F -1 B ∧ t ∈ A
16 13 14 15 3bitr4i ⊢ t ∈ F ↾ A -1 B ↔ t ∈ F -1 B ∩ A
17 16 eqriv ⊢ F ↾ A -1 B = F -1 B ∩ A