Theorem relpart 38058

Description: Two ways of expressing the "relation part" of a class: its restriction to the universal class (that is, its intersection with the Cartesian square of the universal class) equals the class of ordered pairs it contains (the class of ordered pairs whose components are related by it).

The "relation part" of a class is a relation (see df-rel 5657 and relres 5996) and is the largest relation included in that class (that follows from relssresv 38060). Taking the relation part of a class is a projection onto the collection of relations, that is, it is an idempotent operation (residm 6002) with image the collection of relations (by relres 5996 for one inclusion and the forward implication of dfrel3 6194 for the other). As with any projection, a class is in its image if and only if its is a fixpoint of that projection (which is precisely dfrel3 6194).

Other expressions giving the relation part of a class are cnvcnv 6185, coi1res 38066. (Contributed by BJ, 16-Oct-2026.)

Assertion

Ref	Expression
relpart	⊢ (𝐴 ↾ V) = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐴𝑦}

Distinct variable group:   𝑥,𝐴,𝑦

Proof of Theorem relpart

Step	Hyp	Ref	Expression
1		bj-dfres2 38056	. 2 ⊢ (𝐴 ↾ V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑥𝐴𝑦)}
2		vex 3454	. . . . 5 ⊢ 𝑥 ∈ V
3	2	biantrur 540	. . . 4 ⊢ (𝑥𝐴𝑦 ↔ (𝑥 ∈ V ∧ 𝑥𝐴𝑦))
4	3	bicomi 227	. . 3 ⊢ ((𝑥 ∈ V ∧ 𝑥𝐴𝑦) ↔ 𝑥𝐴𝑦)
5	4	opabbii 5171	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑥𝐴𝑦)} = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐴𝑦}
6	1, 5	eqtri 2783	1 ⊢ (𝐴 ↾ V) = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐴𝑦}

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569   ∈ wcel 2144  Vcvv 3450   class class class wbr 5102  {copab 5166   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-in 4090  df-un 4150  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-res 5662

This theorem is used by:  bj-dfrel4v  38061  bj-cnvcnv2  38063  coi1res  38066