Theorem sprsymrelfolem1

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

	Ref	Expression
Hypothesis	sprsymrelfo.q	⊢ 𝑄 = { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) }
Assertion	sprsymrelfolem1	⊢ 𝑄 ∈ 𝒫 ( Pairs ‘ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		sprsymrelfo.q	⊢ 𝑄 = { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) }
2		fvex	⊢ ( Pairs ‘ 𝑉 ) ∈ V
3		ssrab2	⊢ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) } ⊆ ( Pairs ‘ 𝑉 )
4	2 3	elpwi2	⊢ { 𝑞 ∈ ( Pairs ‘ 𝑉 ) ∣ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( 𝑞 = { 𝑎 , 𝑏 } → 𝑎 𝑅 𝑏 ) } ∈ 𝒫 ( Pairs ‘ 𝑉 )
5	1 4	eqeltri	⊢ 𝑄 ∈ 𝒫 ( Pairs ‘ 𝑉 )