Theorem relopabv 5817

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

Syntax hints:  {copab 5204  Rel wrel 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-in 3951  df-ss 3961  df-opab 5205  df-xp 5678  df-rel 5679

This theorem is referenced by:  opabid2  5824  inopab  5825  difopab  5826  difopabOLD  5827  dfres2  6039  cnvopab  6137  funopab  6582  elopabi  8058  relmpoopab  8091  shftfn  15038  cicer  17774  joindmss  18356  meetdmss  18370  lgsquadlem3  27289  tgjustf  28251  perpln1  28488  perpln2  28489  fpwrelmapffslem  32485  fpwrelmap  32486  relfae  33789  satfrel  34900  xpab  35243  vvdifopab  37654  inxprnres  37687  prtlem12  38263  dicvalrelN  40582  diclspsn  40591  dih1dimatlem  40726  rfovcnvf1od  43347