Theorem opabss 2681

Description: The collection of ordered pairs in a class is a subclass of it.

Assertion

Ref	Expression
opabss	⊢ {⟨x, y⟩∣xRy} ⊆ R

Distinct variable groups:   x,R   y,R

Proof of Theorem opabss

Step	Hyp	Ref	Expression
1		df-opab 2680	. . 3 ⊢ {⟨x, y⟩∣xRy} = {z∣∃x∃y(z = ⟨x, y⟩ ⋀ xRy)}
2		eleq1 1541	. . . . . . 7 ⊢ (z = ⟨x, y⟩ → (z ∈ R ↔ ⟨x, y⟩ ∈ R))
3	2	biimpar 419	. . . . . 6 ⊢ ((z = ⟨x, y⟩ ⋀ ⟨x, y⟩ ∈ R) → z ∈ R)
4		df-br 2633	. . . . . 6 ⊢ (xRy ↔ ⟨x, y⟩ ∈ R)
5	3, 4	sylan2b 455	. . . . 5 ⊢ ((z = ⟨x, y⟩ ⋀ xRy) → z ∈ R)
6	5	19.23aivv 1302	. . . 4 ⊢ (∃x∃y(z = ⟨x, y⟩ ⋀ xRy) → z ∈ R)
7	6	ss2abi 2129	. . 3 ⊢ {z∣∃x∃y(z = ⟨x, y⟩ ⋀ xRy)} ⊆ {z∣z ∈ R}
8	1, 7	eqsstr 2100	. 2 ⊢ {⟨x, y⟩∣xRy} ⊆ {z∣z ∈ R}
9		abid2 1587	. 2 ⊢ {z∣z ∈ R} = R
10	8, 9	sseqtr 2102	1 ⊢ {⟨x, y⟩∣xRy} ⊆ R

Syntax hints:   ⋀ wa 223   = wceq 960   ∈ wcel 962  ∃wex 984  {cab 1470   ⊆ wss 2056  ⟨cop 2421   class class class wbr 2632  {copab 2679

This theorem is referenced by:  cotr 3450  cnvsym 3451

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-12 972  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1129  ax-10o 1146  ax-16 1216  ax-11o 1224  ax-ext 1466

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 985  df-sb 1178  df-clab 1471  df-cleq 1476  df-clel 1479  df-in 2060  df-ss 2062  df-br 2633  df-opab 2680

Copyright terms: Public domain