This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )