Theorem relopabv 5795

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

Syntax hints:  {copab 5163  Rel wrel 5653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-opab 5164  df-xp 5654  df-rel 5655

This theorem is referenced by:  opabid2  5802  inopab  5803  difopab  5804  dfres2  6030  cnvopab  6124  funopab  6556  elopabi  8043  relmpoopab  8073  shftfn  15096  cicer  17849  joindmss  18419  meetdmss  18433  lgsquadlem3  27453  tgjustf  28649  perpln1  28890  perpln2  28891  fpwrelmapffslem  32940  fpwrelmap  32941  relfae  34546  satfrel  35722  xpab  36081  vvdifopab  38769  inxprnres  38802  prtlem12  39496  dicvalrelN  41814  diclspsn  41823  dih1dimatlem  41958  rfovcnvf1od  44585