Theorem relopabv 5834

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

Syntax hints:  {copab 5210  Rel wrel 5694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-opab 5211  df-xp 5695  df-rel 5696

This theorem is referenced by:  opabid2  5841  inopab  5842  difopab  5843  difopabOLD  5844  dfres2  6061  cnvopab  6160  cnvopabOLD  6161  funopab  6603  elopabi  8086  relmpoopab  8118  shftfn  15109  cicer  17854  joindmss  18437  meetdmss  18451  lgsquadlem3  27441  tgjustf  28496  perpln1  28733  perpln2  28734  fpwrelmapffslem  32750  fpwrelmap  32751  relfae  34228  satfrel  35352  xpab  35706  vvdifopab  38242  inxprnres  38274  prtlem12  38849  dicvalrelN  41168  diclspsn  41177  dih1dimatlem  41312  rfovcnvf1od  43994