Theorem relopabv 5766

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

Syntax hints:  {copab 5136  Rel wrel 5625

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3429  df-ss 3902  df-opab 5137  df-xp 5626  df-rel 5627

This theorem is referenced by:  opabid2  5773  inopab  5774  difopab  5775  dfres2  5995  cnvopab  6089  cnvopabOLD  6090  funopab  6522  elopabi  8004  relmpoopab  8033  shftfn  15024  cicer  17762  joindmss  18332  meetdmss  18346  lgsquadlem3  27333  tgjustf  28529  perpln1  28766  perpln2  28767  fpwrelmapffslem  32793  fpwrelmap  32794  relfae  34379  satfrel  35537  xpab  35896  vvdifopab  38574  inxprnres  38607  prtlem12  39301  dicvalrelN  41619  diclspsn  41628  dih1dimatlem  41763  rfovcnvf1od  44419