Theorem prssad

Description: If a pair is a subset of a class, the first element of the pair is an element of that class. (Contributed by Thierry Arnoux, 2-Nov-2025)

	Ref	Expression
Hypotheses	prssad.1	|- ( ph -> A e. V )
	prssad.2	|- ( ph -> { A , B } C_ C )
Assertion	prssad	|- ( ph -> A e. C )

Proof

Step	Hyp	Ref	Expression
1		prssad.1	|- ( ph -> A e. V )
2		prssad.2	|- ( ph -> { A , B } C_ C )
3	1	adantr	|- ( ( ph /\ B e. _V ) -> A e. V )
4		simpr	|- ( ( ph /\ B e. _V ) -> B e. _V )
5	2	adantr	|- ( ( ph /\ B e. _V ) -> { A , B } C_ C )
6		prssg	|- ( ( A e. V /\ B e. _V ) -> ( ( A e. C /\ B e. C ) <-> { A , B } C_ C ) )
7	6	biimpar	|- ( ( ( A e. V /\ B e. _V ) /\ { A , B } C_ C ) -> ( A e. C /\ B e. C ) )
8	3 4 5 7	syl21anc	|- ( ( ph /\ B e. _V ) -> ( A e. C /\ B e. C ) )
9	8	simpld	|- ( ( ph /\ B e. _V ) -> A e. C )
10		prprc2	|- ( -. B e. _V -> { A , B } = { A } )
11	10	adantl	|- ( ( ph /\ -. B e. _V ) -> { A , B } = { A } )
12	2	adantr	|- ( ( ph /\ -. B e. _V ) -> { A , B } C_ C )
13	11 12	eqsstrrd	|- ( ( ph /\ -. B e. _V ) -> { A } C_ C )
14		snssg	|- ( A e. V -> ( A e. C <-> { A } C_ C ) )
15	14	biimpar	|- ( ( A e. V /\ { A } C_ C ) -> A e. C )
16	1 13 15	syl2an2r	|- ( ( ph /\ -. B e. _V ) -> A e. C )
17	9 16	pm2.61dan	|- ( ph -> A e. C )