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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	prssad.2	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ 𝐶 )
Assertion	prssad	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		prssad.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		prssad.2	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ 𝐶 )
3	1	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐴 ∈ 𝑉 )
4		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐵 ∈ V )
5	2	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → { 𝐴 , 𝐵 } ⊆ 𝐶 )
6		prssg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ↔ { 𝐴 , 𝐵 } ⊆ 𝐶 ) )
7	6	biimpar	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ V ) ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ) → ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) )
8	3 4 5 7	syl21anc	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) )
9	8	simpld	⊢ ( ( 𝜑 ∧ 𝐵 ∈ V ) → 𝐴 ∈ 𝐶 )
10		prprc2	⊢ ( ¬ 𝐵 ∈ V → { 𝐴 , 𝐵 } = { 𝐴 } )
11	10	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ V ) → { 𝐴 , 𝐵 } = { 𝐴 } )
12	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ V ) → { 𝐴 , 𝐵 } ⊆ 𝐶 )
13	11 12	eqsstrrd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ V ) → { 𝐴 } ⊆ 𝐶 )
14		snssg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝐶 ↔ { 𝐴 } ⊆ 𝐶 ) )
15	14	biimpar	⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝐴 } ⊆ 𝐶 ) → 𝐴 ∈ 𝐶 )
16	1 13 15	syl2an2r	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ V ) → 𝐴 ∈ 𝐶 )
17	9 16	pm2.61dan	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )