Theorem eqrelriiv 5737

Description: Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995.)

Hypotheses

Ref	Expression
eqreliiv.1	⊢ Rel 𝐴
eqreliiv.2	⊢ Rel 𝐵
eqreliiv.3	⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)

Assertion

Ref	Expression
eqrelriiv	⊢ 𝐴 = 𝐵

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Proof of Theorem eqrelriiv

Step	Hyp	Ref	Expression
1		eqreliiv.1	. 2 ⊢ Rel 𝐴
2		eqreliiv.2	. 2 ⊢ Rel 𝐵
3		eqreliiv.3	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)
4	3	eqrelriv 5736	. 2 ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵)
5	1, 2, 4	mp2an 692	1 ⊢ 𝐴 = 𝐵

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ⟨cop 4584  Rel wrel 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-ss 3916  df-opab 5159  df-xp 5628  df-rel 5629

This theorem is referenced by:  eqbrriv  5738  inopab  5776  difopab  5777  inxp  5778  dfres2  5998  restidsing  6010  cnvopab  6092  cnvopabOLD  6093  cnvdif  6099  difxp  6120  cnvcnvsn  6175  dfco2  6201  coiun  6213  co02  6217  coass  6222  ressn  6241  ovoliunlem1  25457  h2hlm  31004  cnvco1  35902  cnvco2  35903  inxprnres  38430  cnviun  43833  coiun1  43835  coxp  49020