Theorem relopabv 5806

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

This proof depends on syntax axioms:  {copab 5171  Rel wrel 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-opab 5172  df-xp 5665  df-rel 5666

This theorem is used by:  opabid2  5813  inopab  5814  difopab  5815  dfres2  6041  cnvopab  6135  funopab  6572  elopabi  8062  relmpoopab  8094  shftfn  15148  cicer  17899  joindmss  18469  meetdmss  18483  lgsquadlem3  27619  tgjustf  28815  perpln1  29065  perpln2  29066  fpwrelmapffslem  33205  fpwrelmap  33206  relfae  34760  satfrel  35948  xpab  36307  vvdifopab  39015  inxprnres  39048  prtlem12  39742  dicvalrelN  42060  diclspsn  42069  dih1dimatlem  42204  rfovcnvf1od  44846