Theorem relopabv 5764

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

Syntax hints:  {copab 5154  Rel wrel 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-opab 5155  df-xp 5625  df-rel 5626

This theorem is referenced by:  opabid2  5771  inopab  5772  difopab  5773  dfres2  5992  cnvopab  6086  cnvopabOLD  6087  funopab  6517  elopabi  7997  relmpoopab  8027  shftfn  14980  cicer  17713  joindmss  18283  meetdmss  18297  lgsquadlem3  27291  tgjustf  28422  perpln1  28659  perpln2  28660  fpwrelmapffslem  32684  fpwrelmap  32685  relfae  34230  satfrel  35360  xpab  35719  vvdifopab  38255  inxprnres  38286  prtlem12  38866  dicvalrelN  41184  diclspsn  41193  dih1dimatlem  41328  rfovcnvf1od  43997