Theorem relopabv 5782

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

Syntax hints:  {copab 5172  Rel wrel 5643

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 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-opab 5173  df-xp 5644  df-rel 5645

This theorem is referenced by:  opabid2  5789  inopab  5790  difopab  5791  difopabOLD  5792  dfres2  6000  cnvopab  6096  funopab  6541  elopabi  7999  relmpoopab  8031  shftfn  14970  cicer  17703  joindmss  18282  meetdmss  18296  lgsquadlem3  26767  tgjustf  27478  perpln1  27715  perpln2  27716  fpwrelmapffslem  31717  fpwrelmap  31718  relfae  32935  satfrel  34048  xpab  34384  vvdifopab  36793  inxprnres  36826  prtlem12  37402  dicvalrelN  39721  diclspsn  39730  dih1dimatlem  39865  rfovcnvf1od  42398