Metamath Proof Explorer

Theorem sprsymrelfolem1

Description: Lemma 1 for sprsymrelfo . (Contributed by AV, 22-Nov-2021)

Ref Expression
Hypothesis sprsymrelfo.q ⊢Q=q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→aRb
Assertion sprsymrelfolem1 ⊢Q∈𝒫Pairs⁡V

Proof

Step Hyp Ref Expression
1 sprsymrelfo.q ⊢Q=q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→aRb
2 fvex ⊢Pairs⁡V∈V
3 ssrab2 ⊢q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→aRb⊆Pairs⁡V
4 2 3 elpwi2 ⊢q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→aRb∈𝒫Pairs⁡V
5 1 4 eqeltri ⊢Q∈𝒫Pairs⁡V