# Metamath Proof Explorer

## Theorem 2elresin

Description: Membership in two functions restricted by each other's domain. (Contributed by NM, 8-Aug-1994)

Ref Expression
Assertion 2elresin ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\right)\to \left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)↔\left(⟨{x},{y}⟩\in \left({{F}↾}_{\left({A}\cap {B}\right)}\right)\wedge ⟨{x},{z}⟩\in \left({{G}↾}_{\left({A}\cap {B}\right)}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 fnop ${⊢}\left({F}Fn{A}\wedge ⟨{x},{y}⟩\in {F}\right)\to {x}\in {A}$
2 fnop ${⊢}\left({G}Fn{B}\wedge ⟨{x},{z}⟩\in {G}\right)\to {x}\in {B}$
3 1 2 anim12i ${⊢}\left(\left({F}Fn{A}\wedge ⟨{x},{y}⟩\in {F}\right)\wedge \left({G}Fn{B}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\to \left({x}\in {A}\wedge {x}\in {B}\right)$
4 3 an4s ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\to \left({x}\in {A}\wedge {x}\in {B}\right)$
5 elin ${⊢}{x}\in \left({A}\cap {B}\right)↔\left({x}\in {A}\wedge {x}\in {B}\right)$
6 4 5 sylibr ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\to {x}\in \left({A}\cap {B}\right)$
7 vex ${⊢}{y}\in \mathrm{V}$
8 7 opres ${⊢}{x}\in \left({A}\cap {B}\right)\to \left(⟨{x},{y}⟩\in \left({{F}↾}_{\left({A}\cap {B}\right)}\right)↔⟨{x},{y}⟩\in {F}\right)$
9 vex ${⊢}{z}\in \mathrm{V}$
10 9 opres ${⊢}{x}\in \left({A}\cap {B}\right)\to \left(⟨{x},{z}⟩\in \left({{G}↾}_{\left({A}\cap {B}\right)}\right)↔⟨{x},{z}⟩\in {G}\right)$
11 8 10 anbi12d ${⊢}{x}\in \left({A}\cap {B}\right)\to \left(\left(⟨{x},{y}⟩\in \left({{F}↾}_{\left({A}\cap {B}\right)}\right)\wedge ⟨{x},{z}⟩\in \left({{G}↾}_{\left({A}\cap {B}\right)}\right)\right)↔\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\right)$
12 11 biimprd ${⊢}{x}\in \left({A}\cap {B}\right)\to \left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\to \left(⟨{x},{y}⟩\in \left({{F}↾}_{\left({A}\cap {B}\right)}\right)\wedge ⟨{x},{z}⟩\in \left({{G}↾}_{\left({A}\cap {B}\right)}\right)\right)\right)$
13 6 12 syl ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\right)\to \left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\to \left(⟨{x},{y}⟩\in \left({{F}↾}_{\left({A}\cap {B}\right)}\right)\wedge ⟨{x},{z}⟩\in \left({{G}↾}_{\left({A}\cap {B}\right)}\right)\right)\right)$
14 13 ex ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\right)\to \left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\to \left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\to \left(⟨{x},{y}⟩\in \left({{F}↾}_{\left({A}\cap {B}\right)}\right)\wedge ⟨{x},{z}⟩\in \left({{G}↾}_{\left({A}\cap {B}\right)}\right)\right)\right)\right)$
15 14 pm2.43d ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\right)\to \left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)\to \left(⟨{x},{y}⟩\in \left({{F}↾}_{\left({A}\cap {B}\right)}\right)\wedge ⟨{x},{z}⟩\in \left({{G}↾}_{\left({A}\cap {B}\right)}\right)\right)\right)$
16 resss ${⊢}{{F}↾}_{\left({A}\cap {B}\right)}\subseteq {F}$
17 16 sseli ${⊢}⟨{x},{y}⟩\in \left({{F}↾}_{\left({A}\cap {B}\right)}\right)\to ⟨{x},{y}⟩\in {F}$
18 resss ${⊢}{{G}↾}_{\left({A}\cap {B}\right)}\subseteq {G}$
19 18 sseli ${⊢}⟨{x},{z}⟩\in \left({{G}↾}_{\left({A}\cap {B}\right)}\right)\to ⟨{x},{z}⟩\in {G}$
20 17 19 anim12i ${⊢}\left(⟨{x},{y}⟩\in \left({{F}↾}_{\left({A}\cap {B}\right)}\right)\wedge ⟨{x},{z}⟩\in \left({{G}↾}_{\left({A}\cap {B}\right)}\right)\right)\to \left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)$
21 15 20 impbid1 ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\right)\to \left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {G}\right)↔\left(⟨{x},{y}⟩\in \left({{F}↾}_{\left({A}\cap {B}\right)}\right)\wedge ⟨{x},{z}⟩\in \left({{G}↾}_{\left({A}\cap {B}\right)}\right)\right)\right)$