Theorem dfid7

Description: Definition of identity relation as the trivial closure. (Contributed by RP, 26-Jul-2020)

	Ref	Expression
Assertion	dfid7	⊢ I = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ⊤ ) } )

Proof

Step	Hyp	Ref	Expression
1		dfid4	⊢ I = ( 𝑥 ∈ V ↦ 𝑥 )
2		ancom	⊢ ( ( 𝑥 ⊆ 𝑦 ∧ ⊤ ) ↔ ( ⊤ ∧ 𝑥 ⊆ 𝑦 ) )
3		truan	⊢ ( ( ⊤ ∧ 𝑥 ⊆ 𝑦 ) ↔ 𝑥 ⊆ 𝑦 )
4	2 3	bitri	⊢ ( ( 𝑥 ⊆ 𝑦 ∧ ⊤ ) ↔ 𝑥 ⊆ 𝑦 )
5	4	abbii	⊢ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ⊤ ) } = { 𝑦 ∣ 𝑥 ⊆ 𝑦 }
6	5	inteqi	⊢ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ⊤ ) } = ∩ { 𝑦 ∣ 𝑥 ⊆ 𝑦 }
7		vex	⊢ 𝑥 ∈ V
8	7	intmin2	⊢ ∩ { 𝑦 ∣ 𝑥 ⊆ 𝑦 } = 𝑥
9	6 8	eqtri	⊢ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ⊤ ) } = 𝑥
10	9	mpteq2i	⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ⊤ ) } ) = ( 𝑥 ∈ V ↦ 𝑥 )
11	1 10	eqtr4i	⊢ I = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ⊤ ) } )