Theorem relopabv 5731

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

Syntax hints:  {copab 5136  Rel wrel 5594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-opab 5137  df-xp 5595  df-rel 5596

This theorem is referenced by:  opabid2  5738  inopab  5739  difopab  5740  dfres2  5949  cnvopab  6042  funopab  6469  elopabi  7902  relmpoopab  7934  shftfn  14784  cicer  17518  joindmss  18097  meetdmss  18111  lgsquadlem3  26530  tgjustf  26834  perpln1  27071  perpln2  27072  fpwrelmapffslem  31067  fpwrelmap  31068  relfae  32215  satfrel  33329  xpab  33677  vvdifopab  36399  inxprnres  36427  prtlem12  36881  dicvalrelN  39199  diclspsn  39208  dih1dimatlem  39343  rfovcnvf1od  41612