# 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 ${⊢}{\left({{F}↾}_{{A}}\right)}^{-1}\left[{B}\right]={{F}}^{-1}\left[{B}\right]\cap {A}$

### Proof

Step Hyp Ref Expression
1 19.41v ${⊢}\exists {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\in {B}\wedge ⟨{s},{t}⟩\in {{F}}^{-1}\right)\wedge {t}\in {A}\right)↔\left(\exists {s}\phantom{\rule{.4em}{0ex}}\left({s}\in {B}\wedge ⟨{s},{t}⟩\in {{F}}^{-1}\right)\wedge {t}\in {A}\right)$
2 vex ${⊢}{s}\in \mathrm{V}$
3 2 opelresi ${⊢}⟨{t},{s}⟩\in \left({{F}↾}_{{A}}\right)↔\left({t}\in {A}\wedge ⟨{t},{s}⟩\in {F}\right)$
4 vex ${⊢}{t}\in \mathrm{V}$
5 2 4 opelcnv ${⊢}⟨{s},{t}⟩\in {\left({{F}↾}_{{A}}\right)}^{-1}↔⟨{t},{s}⟩\in \left({{F}↾}_{{A}}\right)$
6 2 4 opelcnv ${⊢}⟨{s},{t}⟩\in {{F}}^{-1}↔⟨{t},{s}⟩\in {F}$
7 6 anbi2ci ${⊢}\left(⟨{s},{t}⟩\in {{F}}^{-1}\wedge {t}\in {A}\right)↔\left({t}\in {A}\wedge ⟨{t},{s}⟩\in {F}\right)$
8 3 5 7 3bitr4i ${⊢}⟨{s},{t}⟩\in {\left({{F}↾}_{{A}}\right)}^{-1}↔\left(⟨{s},{t}⟩\in {{F}}^{-1}\wedge {t}\in {A}\right)$
9 8 bianass ${⊢}\left({s}\in {B}\wedge ⟨{s},{t}⟩\in {\left({{F}↾}_{{A}}\right)}^{-1}\right)↔\left(\left({s}\in {B}\wedge ⟨{s},{t}⟩\in {{F}}^{-1}\right)\wedge {t}\in {A}\right)$
10 9 exbii ${⊢}\exists {s}\phantom{\rule{.4em}{0ex}}\left({s}\in {B}\wedge ⟨{s},{t}⟩\in {\left({{F}↾}_{{A}}\right)}^{-1}\right)↔\exists {s}\phantom{\rule{.4em}{0ex}}\left(\left({s}\in {B}\wedge ⟨{s},{t}⟩\in {{F}}^{-1}\right)\wedge {t}\in {A}\right)$
11 4 elima3 ${⊢}{t}\in {{F}}^{-1}\left[{B}\right]↔\exists {s}\phantom{\rule{.4em}{0ex}}\left({s}\in {B}\wedge ⟨{s},{t}⟩\in {{F}}^{-1}\right)$
12 11 anbi1i ${⊢}\left({t}\in {{F}}^{-1}\left[{B}\right]\wedge {t}\in {A}\right)↔\left(\exists {s}\phantom{\rule{.4em}{0ex}}\left({s}\in {B}\wedge ⟨{s},{t}⟩\in {{F}}^{-1}\right)\wedge {t}\in {A}\right)$
13 1 10 12 3bitr4i ${⊢}\exists {s}\phantom{\rule{.4em}{0ex}}\left({s}\in {B}\wedge ⟨{s},{t}⟩\in {\left({{F}↾}_{{A}}\right)}^{-1}\right)↔\left({t}\in {{F}}^{-1}\left[{B}\right]\wedge {t}\in {A}\right)$
14 4 elima3 ${⊢}{t}\in {\left({{F}↾}_{{A}}\right)}^{-1}\left[{B}\right]↔\exists {s}\phantom{\rule{.4em}{0ex}}\left({s}\in {B}\wedge ⟨{s},{t}⟩\in {\left({{F}↾}_{{A}}\right)}^{-1}\right)$
15 elin ${⊢}{t}\in \left({{F}}^{-1}\left[{B}\right]\cap {A}\right)↔\left({t}\in {{F}}^{-1}\left[{B}\right]\wedge {t}\in {A}\right)$
16 13 14 15 3bitr4i ${⊢}{t}\in {\left({{F}↾}_{{A}}\right)}^{-1}\left[{B}\right]↔{t}\in \left({{F}}^{-1}\left[{B}\right]\cap {A}\right)$
17 16 eqriv ${⊢}{\left({{F}↾}_{{A}}\right)}^{-1}\left[{B}\right]={{F}}^{-1}\left[{B}\right]\cap {A}$