Theorem opabss

Description: The collection of ordered pairs in a class is a subclass of it. (Contributed by NM, 27-Dec-1996) (Proof shortened by Andrew Salmon, 9-Jul-2011)

	Ref	Expression
Assertion	opabss	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 } ⊆ 𝑅

Proof

Step	Hyp	Ref	Expression
1		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) }
2		df-br	⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
3		eleq1	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
4	3	biimpar	⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) → 𝑧 ∈ 𝑅 )
5	2 4	sylan2b	⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) → 𝑧 ∈ 𝑅 )
6	5	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) → 𝑧 ∈ 𝑅 )
7	6	abssi	⊢ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) } ⊆ 𝑅
8	1 7	eqsstri	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 } ⊆ 𝑅