Theorem dfres4

Description: Alternate definition of the restriction of a class. (Contributed by Peter Mazsa, 2-Jan-2019)

	Ref	Expression
Assertion	dfres4	⊢ ( 𝑅 ↾ 𝐴 ) = ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfres2	⊢ ( 𝑅 ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) }
2		inxprnres	⊢ ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) }
3	1 2	eqtr4i	⊢ ( 𝑅 ↾ 𝐴 ) = ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) )