Theorem eqrelriiv 5735

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

Syntax hints:   ↔ wb 208   = wceq 1548   ∈ wcel 2121  ⟨cop 4563  Rel wrel 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3901  df-opab 5137  df-xp 5626  df-rel 5627

This theorem is referenced by:  eqbrriv  5736  inopab  5774  difopab  5775  inxp  5776  dfres2  5999  restidsing  6011  cnvopab  6093  cnvdif  6096  difxp  6118  cnvcnvsn  6173  dfco2  6199  coiun  6211  co02  6215  coass  6220  ressn  6239  ovoliunlem1  25490  h2hlm  31071  cnvco1  36000  cnvco2  36001  inxprnres  38678  cnviun  44107  coiun1  44109  coxp  49335