Theorem bj-dfid2ALT

Description: Alternate version of dfid2 . (Contributed by BJ, 9-Nov-2024) (Proof modification is discouraged.) Use df-id instead to make the semantics of the construction df-opab clearer. (New usage is discouraged.)

	Ref	Expression
Assertion	bj-dfid2ALT	⊢ I = { ⟨ 𝑥 , 𝑥 ⟩ ∣ ⊤ }

Proof

Step	Hyp	Ref	Expression
1		df-id	⊢ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 }
2		equcomi	⊢ ( 𝑥 = 𝑦 → 𝑦 = 𝑥 )
3	2	opeq2d	⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑥 ⟩ )
4	3	eqeq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ) )
5	4	pm5.32ri	⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑦 ) )
6	5	exbii	⊢ ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑦 ) )
7		ax6evr	⊢ ∃ 𝑦 𝑥 = 𝑦
8		19.42v	⊢ ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑦 ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ ∃ 𝑦 𝑥 = 𝑦 ) )
9	7 8	mpbiran2	⊢ ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑦 ) ↔ 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ )
10	6 9	bitri	⊢ ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ↔ 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ )
11	10	exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ↔ ∃ 𝑥 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ )
12		id	⊢ ( 𝑥 = 𝑢 → 𝑥 = 𝑢 )
13	12 12	opeq12d	⊢ ( 𝑥 = 𝑢 → ⟨ 𝑥 , 𝑥 ⟩ = ⟨ 𝑢 , 𝑢 ⟩ )
14	13	eqeq2d	⊢ ( 𝑥 = 𝑢 → ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ↔ 𝑧 = ⟨ 𝑢 , 𝑢 ⟩ ) )
15	14	exexw	⊢ ( ∃ 𝑥 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ↔ ∃ 𝑥 ∃ 𝑥 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ )
16	11 15	bitri	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ↔ ∃ 𝑥 ∃ 𝑥 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ )
17		tru	⊢ ⊤
18	17	biantru	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ↔ ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ ⊤ ) )
19	18	exbii	⊢ ( ∃ 𝑥 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ↔ ∃ 𝑥 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ ⊤ ) )
20	19	exbii	⊢ ( ∃ 𝑥 ∃ 𝑥 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ↔ ∃ 𝑥 ∃ 𝑥 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ ⊤ ) )
21	16 20	bitri	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ↔ ∃ 𝑥 ∃ 𝑥 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ ⊤ ) )
22	21	abbii	⊢ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑥 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ ⊤ ) }
23		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) }
24		df-opab	⊢ { ⟨ 𝑥 , 𝑥 ⟩ ∣ ⊤ } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑥 ( 𝑧 = ⟨ 𝑥 , 𝑥 ⟩ ∧ ⊤ ) }
25	22 23 24	3eqtr4i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } = { ⟨ 𝑥 , 𝑥 ⟩ ∣ ⊤ }
26	1 25	eqtri	⊢ I = { ⟨ 𝑥 , 𝑥 ⟩ ∣ ⊤ }