Metamath Proof Explorer

Theorem br1cnvssrres

Description: Restricted converse subset binary relation. (Contributed by Peter Mazsa, 25-Nov-2019)

Ref Expression
Assertion br1cnvssrres ⊢ B ∈ V → B S ↾ A -1 C ↔ C ∈ A ∧ C ⊆ B

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ⁡ S ↾ A
2 1 relbrcnv ⊢ B S ↾ A -1 C ↔ C S ↾ A B
3 brssrres ⊢ B ∈ V → C S ↾ A B ↔ C ∈ A ∧ C ⊆ B
4 2 3 bitrid ⊢ B ∈ V → B S ↾ A -1 C ↔ C ∈ A ∧ C ⊆ B