Theorem imai 5618

Description: Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38. (Contributed by NM, 30-Apr-1998.)

Assertion

Ref	Expression
imai	⊢ ( I “ 𝐴) = 𝐴

Proof of Theorem imai

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfima3 5609	. 2 ⊢ ( I “ 𝐴) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ I )}
2		df-br 4788	. . . . . . . 8 ⊢ (𝑥 I 𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ I )
3		vex 3354	. . . . . . . . 9 ⊢ 𝑦 ∈ V
4	3	ideq 5412	. . . . . . . 8 ⊢ (𝑥 I 𝑦 ↔ 𝑥 = 𝑦)
5	2, 4	bitr3i 266	. . . . . . 7 ⊢ (⟨𝑥, 𝑦⟩ ∈ I ↔ 𝑥 = 𝑦)
6	5	anbi2i 609	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ I ) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 = 𝑦))
7		ancom 448	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 = 𝑦) ↔ (𝑥 = 𝑦 ∧ 𝑥 ∈ 𝐴))
8	6, 7	bitri 264	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ I ) ↔ (𝑥 = 𝑦 ∧ 𝑥 ∈ 𝐴))
9	8	exbii 1924	. . . 4 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ I ) ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝑥 ∈ 𝐴))
10		eleq1w 2833	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
11	10	equsexvw 2090	. . . 4 ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝑥 ∈ 𝐴) ↔ 𝑦 ∈ 𝐴)
12	9, 11	bitri 264	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ I ) ↔ 𝑦 ∈ 𝐴)
13	12	abbii 2888	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ I )} = {𝑦 ∣ 𝑦 ∈ 𝐴}
14		abid2 2894	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴
15	1, 13, 14	3eqtri 2797	1 ⊢ ( I “ 𝐴) = 𝐴

Syntax hints:   ∧ wa 382   = wceq 1631  ∃wex 1852   ∈ wcel 2145  {cab 2757  ⟨cop 4323   class class class wbr 4787   I cid 5157   “ cima 5253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pr 5035

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-br 4788  df-opab 4848  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263

This theorem is referenced by:  rnresi  5619  cnvresid  6107  ecidsn  7951  mbfid  23623  frege131d  38582  frege110  38793  frege133  38816