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	$$⊢\phi \to A\in V$$
	prssad.2	$$⊢\phi \to \left\{A,B\right\}\subseteq C$$
Assertion	prssad	$$⊢\phi \to A\in C$$

Proof

Step	Hyp	Ref	Expression
1		prssad.1	$$⊢\phi \to A\in V$$
2		prssad.2	$$⊢\phi \to \left\{A,B\right\}\subseteq C$$
3	1	adantr	$$⊢\left(\phi \wedge B\in \mathrm{V}\right)\to A\in V$$
4		simpr	$$⊢\left(\phi \wedge B\in \mathrm{V}\right)\to B\in \mathrm{V}$$
5	2	adantr	$$⊢\left(\phi \wedge B\in \mathrm{V}\right)\to \left\{A,B\right\}\subseteq C$$
6		prssg	$$⊢\left(A\in V\wedge B\in \mathrm{V}\right)\to \left(\left(A\in C\wedge B\in C\right)\leftrightarrow \left\{A,B\right\}\subseteq C\right)$$
7	6	biimpar	$$⊢\left(\left(A\in V\wedge B\in \mathrm{V}\right)\wedge \left\{A,B\right\}\subseteq C\right)\to \left(A\in C\wedge B\in C\right)$$
8	3 4 5 7	syl21anc	$$⊢\left(\phi \wedge B\in \mathrm{V}\right)\to \left(A\in C\wedge B\in C\right)$$
9	8	simpld	$$⊢\left(\phi \wedge B\in \mathrm{V}\right)\to A\in C$$
10		prprc2	$$⊢\neg B\in \mathrm{V}\to \left\{A,B\right\}=\left\{A\right\}$$
11	10	adantl	$$⊢\left(\phi \wedge \neg B\in \mathrm{V}\right)\to \left\{A,B\right\}=\left\{A\right\}$$
12	2	adantr	$$⊢\left(\phi \wedge \neg B\in \mathrm{V}\right)\to \left\{A,B\right\}\subseteq C$$
13	11 12	eqsstrrd	$$⊢\left(\phi \wedge \neg B\in \mathrm{V}\right)\to \left\{A\right\}\subseteq C$$
14		snssg	$$⊢A\in V\to \left(A\in C\leftrightarrow \left\{A\right\}\subseteq C\right)$$
15	14	biimpar	$$⊢\left(A\in V\wedge \left\{A\right\}\subseteq C\right)\to A\in C$$
16	1 13 15	syl2an2r	$$⊢\left(\phi \wedge \neg B\in \mathrm{V}\right)\to A\in C$$
17	9 16	pm2.61dan	$$⊢\phi \to A\in C$$