Theorem dfid6

Description: Identity relation expressed as indexed union of relational powers. (Contributed by RP, 9-Jun-2020)

	Ref	Expression
Assertion	dfid6	⊢ I = ( 𝑥 ∈ V ↦ ∪ 𝑛 ∈ { 1 } ( 𝑥 ↑𝑟 𝑛 ) )

Proof

Step	Hyp	Ref	Expression
1		dfid4	⊢ I = ( 𝑥 ∈ V ↦ 𝑥 )
2		1ex	⊢ 1 ∈ V
3		oveq2	⊢ ( 𝑛 = 1 → ( 𝑥 ↑𝑟 𝑛 ) = ( 𝑥 ↑𝑟 1 ) )
4	2 3	iunxsn	⊢ ∪ 𝑛 ∈ { 1 } ( 𝑥 ↑𝑟 𝑛 ) = ( 𝑥 ↑𝑟 1 )
5		relexp1g	⊢ ( 𝑥 ∈ V → ( 𝑥 ↑𝑟 1 ) = 𝑥 )
6	4 5	eqtrid	⊢ ( 𝑥 ∈ V → ∪ 𝑛 ∈ { 1 } ( 𝑥 ↑𝑟 𝑛 ) = 𝑥 )
7	6	mpteq2ia	⊢ ( 𝑥 ∈ V ↦ ∪ 𝑛 ∈ { 1 } ( 𝑥 ↑𝑟 𝑛 ) ) = ( 𝑥 ∈ V ↦ 𝑥 )
8	1 7	eqtr4i	⊢ I = ( 𝑥 ∈ V ↦ ∪ 𝑛 ∈ { 1 } ( 𝑥 ↑𝑟 𝑛 ) )