Theorem relopabv 5724

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

Syntax hints:  {copab 5135  Rel wrel 5589

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 3431  df-in 3893  df-ss 3903  df-opab 5136  df-xp 5590  df-rel 5591

This theorem is referenced by:  opabid2  5731  inopab  5732  difopab  5733  dfres2  5942  cnvopab  6035  funopab  6461  elopabi  7891  relmpoopab  7921  shftfn  14794  cicer  17528  joindmss  18107  meetdmss  18121  lgsquadlem3  26540  tgjustf  26844  perpln1  27081  perpln2  27082  fpwrelmapffslem  31075  fpwrelmap  31076  relfae  32223  satfrel  33337  xpab  33685  vvdifopab  36407  inxprnres  36435  prtlem12  36889  dicvalrelN  39207  diclspsn  39216  dih1dimatlem  39351  rfovcnvf1od  41593