Theorem bj-resssxp

Description: A class is equal to its restriction to some class if and only if it is included in the Cartesian product of the restricting class with the universal class. More fundamental form of resssxp (or at least, more entitled than it to that label). Can shorten relssres through the equivalence |- ( ( Rel A /\ dom A C_ B ) <-> A C_ ( B X. _V ) ) , which could itself be added to set.mm. (Contributed by BJ, 26-Oct-2026)

	Ref	Expression
Assertion	bj-resssxp	⊢ ( ( 𝑅 ↾ 𝐴 ) = 𝑅 ↔ 𝑅 ⊆ ( 𝐴 × V ) )

Proof

Step	Hyp	Ref	Expression
1		df-res	⊢ ( 𝑅 ↾ 𝐴 ) = ( 𝑅 ∩ ( 𝐴 × V ) )
2	1	eqeq1i	⊢ ( ( 𝑅 ↾ 𝐴 ) = 𝑅 ↔ ( 𝑅 ∩ ( 𝐴 × V ) ) = 𝑅 )
3		dfss2	⊢ ( 𝑅 ⊆ ( 𝐴 × V ) ↔ ( 𝑅 ∩ ( 𝐴 × V ) ) = 𝑅 )
4	2 3	bitr4i	⊢ ( ( 𝑅 ↾ 𝐴 ) = 𝑅 ↔ 𝑅 ⊆ ( 𝐴 × V ) )