Theorem eqrelriiv 5762

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 5761	. 2 ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵)
5	1, 2, 4	mp2an 702	1 ⊢ 𝐴 = 𝐵

Syntax hints:   ↔ wb 208   = wceq 1560   ∈ wcel 2142  ⟨cop 4588  Rel wrel 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-opab 5163  df-xp 5653  df-rel 5654

This theorem is referenced by:  eqbrriv  5763  inopab  5802  difopab  5803  inxp  5804  dfres2  6030  restidsing  6042  cnvopab  6124  cnvdif  6127  difxp  6149  cnvcnvsn  6206  dfco2  6232  coiun  6244  co02  6248  coass  6253  ressn  6272  ovoliunlem1  25564  h2hlm  31183  cnvco1  36109  cnvco2  36110  inxprnres  38797  cnviun  44226  coiun1  44228  coxp  49454