Theorem relopab 5395

Description: A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.) Removed DV restrictions. (Revised 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 2752	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
2	1	relopabi 5393	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Syntax hints:  {copab 4856  Rel wrel 5263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-opab 4857  df-xp 5264  df-rel 5265

This theorem is referenced by:  opabid2  5399  inopab  5400  difopab  5401  dfres2  5603  cnvopab  5683  funopab  6076  relmptopab  7040  elopabi  7391  relmpt2opab  7419  shftfn  14004  cicer  16659  joindmss  17200  meetdmss  17214  lgsquadlem3  25298  perpln1  25796  perpln2  25797  fpwrelmapffslem  29808  fpwrelmap  29809  relfae  30611  vvdifopab  34340  inxprnres  34376  prtlem12  34648  dicvalrelN  36968  diclspsn  36977  dih1dimatlem  37112  rfovcnvf1od  38792