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

Metamath Proof Explorer

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 ⊢ φ → B ∈ V
prssbd.2 ⊢ φ → A B ⊆ C
Assertion prssbd ⊢ φ → B ∈ C

Proof

Step Hyp Ref Expression
1 prssbd.1 ⊢ φ → B ∈ V
2 prssbd.2 ⊢ φ → A B ⊆ C
3 simpr ⊢ φ ∧ A ∈ V → A ∈ V
4 1 adantr ⊢ φ ∧ A ∈ V → B ∈ V
5 2 adantr ⊢ φ ∧ A ∈ V → A B ⊆ C
6 prssg ⊢ A ∈ V ∧ B ∈ V → A ∈ C ∧ B ∈ C ↔ A B ⊆ C
7 6 biimpar ⊢ A ∈ V ∧ B ∈ V ∧ A B ⊆ C → A ∈ C ∧ B ∈ C
8 3 4 5 7 syl21anc ⊢ φ ∧ A ∈ V → A ∈ C ∧ B ∈ C
9 8 simprd ⊢ φ ∧ A ∈ V → B ∈ C
10 prprc1 ⊢ ¬ A ∈ V → A B = B
11 10 adantl ⊢ φ ∧ ¬ A ∈ V → A B = B
12 2 adantr ⊢ φ ∧ ¬ A ∈ V → A B ⊆ C
13 11 12 eqsstrrd ⊢ φ ∧ ¬ A ∈ V → B ⊆ C
14 snssg ⊢ B ∈ V → B ∈ C ↔ B ⊆ C
15 14 biimpar ⊢ B ∈ V ∧ B ⊆ C → B ∈ C
16 1 13 15 syl2an2r ⊢ φ ∧ ¬ A ∈ V → B ∈ C
17 9 16 pm2.61dan ⊢ φ → B ∈ C