Theorem prssbd

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

	Ref	Expression
Hypotheses	prssbd.1	$$⊢\phi \to B\in V$$
	prssbd.2	$$⊢\phi \to \left\{A,B\right\}\subseteq C$$
Assertion	prssbd	$$⊢\phi \to B\in C$$

Proof

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