Theorem rabsspr

Description: Conditions for a restricted class abstraction to be a subset of an unordered pair. (Contributed by Thierry Arnoux, 6-Jul-2025)

	Ref	Expression
Assertion	rabsspr	|- ( { x e. V | ph } C_ { X , Y } <-> A. x e. V ( ph -> ( x = X \/ x = Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-rab	|- { x e. V | ph } = { x | ( x e. V /\ ph ) }
2		dfpr2	|- { X , Y } = { x | ( x = X \/ x = Y ) }
3	1 2	sseq12i	|- ( { x e. V | ph } C_ { X , Y } <-> { x | ( x e. V /\ ph ) } C_ { x | ( x = X \/ x = Y ) } )
4		ss2ab	|- ( { x | ( x e. V /\ ph ) } C_ { x | ( x = X \/ x = Y ) } <-> A. x ( ( x e. V /\ ph ) -> ( x = X \/ x = Y ) ) )
5		impexp	|- ( ( ( x e. V /\ ph ) -> ( x = X \/ x = Y ) ) <-> ( x e. V -> ( ph -> ( x = X \/ x = Y ) ) ) )
6	5	albii	|- ( A. x ( ( x e. V /\ ph ) -> ( x = X \/ x = Y ) ) <-> A. x ( x e. V -> ( ph -> ( x = X \/ x = Y ) ) ) )
7		df-ral	|- ( A. x e. V ( ph -> ( x = X \/ x = Y ) ) <-> A. x ( x e. V -> ( ph -> ( x = X \/ x = Y ) ) ) )
8	6 7	bitr4i	|- ( A. x ( ( x e. V /\ ph ) -> ( x = X \/ x = Y ) ) <-> A. x e. V ( ph -> ( x = X \/ x = Y ) ) )
9	3 4 8	3bitri	|- ( { x e. V | ph } C_ { X , Y } <-> A. x e. V ( ph -> ( x = X \/ x = Y ) ) )