Theorem relopabv 5775

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 5778. (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 5774	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Syntax hints:  {copab 5164  Rel wrel 5636

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 3446  df-ss 3928  df-opab 5165  df-xp 5637  df-rel 5638

This theorem is referenced by:  opabid2  5782  inopab  5783  difopab  5784  dfres2  6001  cnvopab  6098  cnvopabOLD  6099  funopab  6535  elopabi  8020  relmpoopab  8050  shftfn  15015  cicer  17748  joindmss  18318  meetdmss  18332  lgsquadlem3  27326  tgjustf  28453  perpln1  28690  perpln2  28691  fpwrelmapffslem  32705  fpwrelmap  32706  relfae  34230  satfrel  35347  xpab  35706  vvdifopab  38242  inxprnres  38273  prtlem12  38853  dicvalrelN  41172  diclspsn  41181  dih1dimatlem  41316  rfovcnvf1od  43986