Theorem relopab 5169

Description: A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.) (Unnecessary distinct variable restrictions were removed by Alan Sare, 9-Jul-2013.) (Proof shortened by Mario Carneiro, 21-Dec-2013.)

Assertion

Ref	Expression
relopab	⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Proof of Theorem relopab

Step	Hyp	Ref	Expression
1		eqid 2610	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2	1	relopabi 5167	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Syntax hints:  {copab 4642  Rel wrel 5043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-opab 4644  df-xp 5044  df-rel 5045

This theorem is referenced by:  opabid2  5173  inopab  5174  difopab  5175  dfres2  5372  cnvopab  5452  funopab  5837  relmptopab  6781  elopabi  7120  relmpt2opab  7146  shftfn  13661  cicer  16289  joindmss  16830  meetdmss  16844  lgsquadlem3  24907  perpln1  25405  perpln2  25406  fpwrelmapffslem  28895  fpwrelmap  28896  relfae  29637  prtlem12  33170  dicvalrelN  35492  diclspsn  35501  dih1dimatlem  35636  rfovcnvf1od  37318