Theorem relopabv 5760

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but using ax-11 2160 and ax-12 2180, see relopab 5763. (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 2731	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2	1	relopabiv 5759	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Syntax hints:  {copab 5151  Rel wrel 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-opab 5152  df-xp 5620  df-rel 5621

This theorem is referenced by:  opabid2  5767  inopab  5768  difopab  5769  dfres2  5989  cnvopab  6083  cnvopabOLD  6084  funopab  6516  elopabi  7994  relmpoopab  8024  shftfn  14980  cicer  17713  joindmss  18283  meetdmss  18297  lgsquadlem3  27320  tgjustf  28451  perpln1  28688  perpln2  28689  fpwrelmapffslem  32715  fpwrelmap  32716  relfae  34260  satfrel  35411  xpab  35770  vvdifopab  38296  inxprnres  38329  prtlem12  38965  dicvalrelN  41283  diclspsn  41292  dih1dimatlem  41427  rfovcnvf1od  44096