Theorem relopabv 5768

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 2185, see relopab 5771. (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 2737	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2	1	relopabiv 5767	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Syntax hints:  {copab 5148  Rel wrel 5627

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-opab 5149  df-xp 5628  df-rel 5629

This theorem is referenced by:  opabid2  5775  inopab  5776  difopab  5777  dfres2  5998  cnvopab  6092  cnvopabOLD  6093  funopab  6525  elopabi  8006  relmpoopab  8035  shftfn  14997  cicer  17731  joindmss  18301  meetdmss  18315  lgsquadlem3  27333  tgjustf  28529  perpln1  28766  perpln2  28767  fpwrelmapffslem  32794  fpwrelmap  32795  relfae  34397  satfrel  35555  xpab  35914  vvdifopab  38577  inxprnres  38610  prtlem12  39304  dicvalrelN  41622  diclspsn  41631  dih1dimatlem  41766  rfovcnvf1od  44434