Theorem rabsstp

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

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

Proof

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