Theorem relopabv 5769

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but using ax-11 2163 and ax-12 2183, see relopab 5772. (Contributed by SN, 8-Sep-2024.)

Assertion

Ref	Expression
relopabv	⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem relopabv

Step	Hyp	Ref	Expression
1		eqid 2735	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2	1	relopabiv 5768	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Syntax hints:  {copab 5159  Rel wrel 5628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3441  df-ss 3917  df-opab 5160  df-xp 5629  df-rel 5630

This theorem is referenced by:  opabid2  5776  inopab  5777  difopab  5778  dfres2  5999  cnvopab  6093  cnvopabOLD  6094  funopab  6526  elopabi  8006  relmpoopab  8036  shftfn  14998  cicer  17732  joindmss  18302  meetdmss  18316  lgsquadlem3  27351  tgjustf  28526  perpln1  28763  perpln2  28764  fpwrelmapffslem  32790  fpwrelmap  32791  relfae  34383  satfrel  35540  xpab  35899  vvdifopab  38435  inxprnres  38468  prtlem12  39162  dicvalrelN  41480  diclspsn  41489  dih1dimatlem  41624  rfovcnvf1od  44282