Theorem relopabv 5805

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

Syntax hints:  {copab 5186  Rel wrel 5664

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-ss 3948  df-opab 5187  df-xp 5665  df-rel 5666

This theorem is referenced by:  opabid2  5812  inopab  5813  difopab  5814  difopabOLD  5815  dfres2  6033  cnvopab  6131  cnvopabOLD  6132  funopab  6576  elopabi  8066  relmpoopab  8098  shftfn  15097  cicer  17824  joindmss  18394  meetdmss  18408  lgsquadlem3  27350  tgjustf  28457  perpln1  28694  perpln2  28695  fpwrelmapffslem  32714  fpwrelmap  32715  relfae  34283  satfrel  35394  xpab  35748  vvdifopab  38283  inxprnres  38315  prtlem12  38890  dicvalrelN  41209  diclspsn  41218  dih1dimatlem  41353  rfovcnvf1od  43995