reldm

Description: An expression for the domain of a relation. (Contributed by NM, 22-Sep-2013) (Proof shortened by Sky Winter, 22-Oct-2026)

		Ref	Expression
	Assertion	reldm	⊢ ( Rel 𝐴 → dom 𝐴 = ran ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) )

Step	Hyp	Ref	Expression
1		releldm2	⊢ ( Rel 𝐴 → ( 𝑦 ∈ dom 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ( 1^st ‘ 𝑥 ) = 𝑦 ) )
2		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) )
3		fvex	⊢ ( 1^st ‘ 𝑥 ) ∈ V
4	2 3	elrnmpti	⊢ ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 1^st ‘ 𝑥 ) )
5		eqcom	⊢ ( 𝑦 = ( 1^st ‘ 𝑥 ) ↔ ( 1^st ‘ 𝑥 ) = 𝑦 )
6	5	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 1^st ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 1^st ‘ 𝑥 ) = 𝑦 )
7	4 6	bitri	⊢ ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ( 1^st ‘ 𝑥 ) = 𝑦 )
8	1 7	bitr4di	⊢ ( Rel 𝐴 → ( 𝑦 ∈ dom 𝐴 ↔ 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) ) )
9	8	eqrdv	⊢ ( Rel 𝐴 → dom 𝐴 = ran ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) )

Metamath Proof Explorer