Theorem relopabv 5845

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

Syntax hints:  {copab 5228  Rel wrel 5705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-opab 5229  df-xp 5706  df-rel 5707

This theorem is referenced by:  opabid2  5852  inopab  5853  difopab  5854  difopabOLD  5855  dfres2  6070  cnvopab  6169  cnvopabOLD  6170  funopab  6613  elopabi  8103  relmpoopab  8135  shftfn  15122  cicer  17867  joindmss  18449  meetdmss  18463  lgsquadlem3  27444  tgjustf  28499  perpln1  28736  perpln2  28737  fpwrelmapffslem  32746  fpwrelmap  32747  relfae  34211  satfrel  35335  xpab  35688  vvdifopab  38216  inxprnres  38248  prtlem12  38823  dicvalrelN  41142  diclspsn  41151  dih1dimatlem  41286  rfovcnvf1od  43966