Theorem resieq 3433

Description: A restricted identity relation is equivalent to equality in its domain.

Assertion

Ref	Expression
resieq	⊢ ((B ∈ A ⋀ C ∈ A) → (B(I ↾ A)C ↔ B = C))

Proof of Theorem resieq

Step	Hyp	Ref	Expression
1		breq2 2678	. . . . 5 ⊢ (x = C → (B(I ↾ A)x ↔ B(I ↾ A)C))
2		eqeq2 1531	. . . . 5 ⊢ (x = C → (B = x ↔ B = C))
3	1, 2	bibi12d 640	. . . 4 ⊢ (x = C → ((B(I ↾ A)x ↔ B = x) ↔ (B(I ↾ A)C ↔ B = C)))
4	3	imbi2d 623	. . 3 ⊢ (x = C → ((B ∈ A → (B(I ↾ A)x ↔ B = x)) ↔ (B ∈ A → (B(I ↾ A)C ↔ B = C))))
5		visset 1860	. . . . 5 ⊢ x ∈ V
6	5	opres 3432	. . . 4 ⊢ (B ∈ A → (⟨B, x⟩ ∈ (I ↾ A) ↔ ⟨B, x⟩ ∈ I))
7		df-br 2675	. . . 4 ⊢ (B(I ↾ A)x ↔ ⟨B, x⟩ ∈ (I ↾ A))
8	5	ideq 3334	. . . . 5 ⊢ (BIx ↔ B = x)
9		df-br 2675	. . . . 5 ⊢ (BIx ↔ ⟨B, x⟩ ∈ I)
10	8, 9	bitr3i 182	. . . 4 ⊢ (B = x ↔ ⟨B, x⟩ ∈ I)
11	6, 7, 10	3bitr4g 566	. . 3 ⊢ (B ∈ A → (B(I ↾ A)x ↔ B = x))
12	4, 11	vtoclg 1894	. 2 ⊢ (C ∈ A → (B ∈ A → (B(I ↾ A)C ↔ B = C)))
13	12	impcom 358	1 ⊢ ((B ∈ A ⋀ C ∈ A) → (B(I ↾ A)C ↔ B = C))

Syntax hints:   → wi 3   ↔ wb 153   ⋀ wa 230   = wceq 997   ∈ wcel 999  ⟨cop 2463   class class class wbr 2674  Icid 2887   ↾ cres 3229

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-pr 2835

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-br 2675  df-opab 2722  df-id 2891  df-xp 3241  df-rel 3242  df-res 3247

Copyright terms: Public domain