Theorem relopabv 5771

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 5774. (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 5770	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Syntax hints:  {copab 5161  Rel wrel 5630

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 3443  df-ss 3919  df-opab 5162  df-xp 5631  df-rel 5632

This theorem is referenced by:  opabid2  5778  inopab  5779  difopab  5780  dfres2  6001  cnvopab  6095  cnvopabOLD  6096  funopab  6528  elopabi  8009  relmpoopab  8039  shftfn  15001  cicer  17735  joindmss  18305  meetdmss  18319  lgsquadlem3  27354  tgjustf  28550  perpln1  28787  perpln2  28788  fpwrelmapffslem  32814  fpwrelmap  32815  relfae  34417  satfrel  35574  xpab  35933  vvdifopab  38479  inxprnres  38512  prtlem12  39206  dicvalrelN  41524  diclspsn  41533  dih1dimatlem  41668  rfovcnvf1od  44323