Theorem relopabv 5821

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 5824. (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 2732	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2	1	relopabiv 5820	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Syntax hints:  {copab 5210  Rel wrel 5681

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-opab 5211  df-xp 5682  df-rel 5683

This theorem is referenced by:  opabid2  5828  inopab  5829  difopab  5830  difopabOLD  5831  dfres2  6041  cnvopab  6138  funopab  6583  elopabi  8050  relmpoopab  8082  shftfn  15022  cicer  17755  joindmss  18334  meetdmss  18348  lgsquadlem3  26892  tgjustf  27762  perpln1  27999  perpln2  28000  fpwrelmapffslem  31995  fpwrelmap  31996  relfae  33314  satfrel  34427  xpab  34764  vvdifopab  37214  inxprnres  37247  prtlem12  37823  dicvalrelN  40142  diclspsn  40151  dih1dimatlem  40286  rfovcnvf1od  42837