Theorem relopabv 5720

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but using ax-11 2156 and ax-12 2173, see relopab 5723. (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 5719	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Syntax hints:  {copab 5132  Rel wrel 5585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-opab 5133  df-xp 5586  df-rel 5587

This theorem is referenced by:  opabid2  5727  inopab  5728  difopab  5729  dfres2  5938  cnvopab  6031  funopab  6453  elopabi  7875  relmpoopab  7905  shftfn  14712  cicer  17435  joindmss  18012  meetdmss  18026  lgsquadlem3  26435  tgjustf  26738  perpln1  26975  perpln2  26976  fpwrelmapffslem  30969  fpwrelmap  30970  relfae  32115  satfrel  33229  xpab  33579  vvdifopab  36326  inxprnres  36354  prtlem12  36808  dicvalrelN  39126  diclspsn  39135  dih1dimatlem  39270  rfovcnvf1od  41501