Theorem coi1 4779

Description: Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.)

Assertion

Ref	Expression
coi1	⊢ (Rel A → (A ∘ I ) = A)

Proof of Theorem coi1

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relco 4762	. 2 ⊢ Rel (A ∘ I )
2		vex 2554	. . . . . 6 ⊢ x ∈ V
3		vex 2554	. . . . . 6 ⊢ y ∈ V
4	2, 3	opelco 4450	. . . . 5 ⊢ (⟨x, y⟩ ∈ (A ∘ I ) ↔ ∃z(x I z ∧ zAy))
5		vex 2554	. . . . . . . . . 10 ⊢ z ∈ V
6	5	ideq 4431	. . . . . . . . 9 ⊢ (x I z ↔ x = z)
7		equcom 1590	. . . . . . . . 9 ⊢ (x = z ↔ z = x)
8	6, 7	bitri 173	. . . . . . . 8 ⊢ (x I z ↔ z = x)
9	8	anbi1i 431	. . . . . . 7 ⊢ ((x I z ∧ zAy) ↔ (z = x ∧ zAy))
10	9	exbii 1493	. . . . . 6 ⊢ (∃z(x I z ∧ zAy) ↔ ∃z(z = x ∧ zAy))
11		breq1 3758	. . . . . . 7 ⊢ (z = x → (zAy ↔ xAy))
12	2, 11	ceqsexv 2587	. . . . . 6 ⊢ (∃z(z = x ∧ zAy) ↔ xAy)
13	10, 12	bitri 173	. . . . 5 ⊢ (∃z(x I z ∧ zAy) ↔ xAy)
14	4, 13	bitri 173	. . . 4 ⊢ (⟨x, y⟩ ∈ (A ∘ I ) ↔ xAy)
15		df-br 3756	. . . 4 ⊢ (xAy ↔ ⟨x, y⟩ ∈ A)
16	14, 15	bitri 173	. . 3 ⊢ (⟨x, y⟩ ∈ (A ∘ I ) ↔ ⟨x, y⟩ ∈ A)
17	16	eqrelriv 4376	. 2 ⊢ ((Rel (A ∘ I ) ∧ Rel A) → (A ∘ I ) = A)
18	1, 17	mpan 400	1 ⊢ (Rel A → (A ∘ I ) = A)

Syntax hints:   → wi 4   ∧ wa 97   = wceq 1242  ∃wex 1378   ∈ wcel 1390  ⟨cop 3370   class class class wbr 3755   I cid 4016   ∘ ccom 4292  Rel wrel 4293

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-id 4021  df-xp 4294  df-rel 4295  df-co 4297

This theorem is referenced by:  coi2  4780  coires1  4781  relcoi1  4792  fcoi1  5013