Theorem cnvresima 6183

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

Assertion

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

Proof of Theorem cnvresima

Dummy variables 𝑡 𝑠 are mutually distinct and distinct from all other variables.

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

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ∩ cin 3884  ⟨cop 4563  ^◡ccnv 5619   ↾ cres 5622   “ cima 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5220  ax-pr 5364

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-xp 5626  df-cnv 5628  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633

This theorem is referenced by:  fimacnvinrn  7012  ramub2  16974  ramub1lem2  16987  cnrest  23238  kgencn  23509  kgencn3  23511  xkoptsub  23607  qtopres  23651  qtoprest  23670  mbfid  25590  mbfres  25599  1stpreima  32768  2ndpreima  32769  gsumhashmul  33116  cvmsss2  35444  lmhmlnmsplit  43503