Theorem eqrelriiv 5777

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

Syntax hints:   ↔ wb 209   = wceq 1567   ∈ wcel 2149  ⟨cop 4600  Rel wrel 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-opab 5178  df-xp 5668  df-rel 5669

This theorem is referenced by:  eqbrriv  5778  inopab  5817  difopab  5818  inxp  5819  dfres2  6044  restidsing  6056  cnvopab  6138  cnvdif  6141  difxp  6162  cnvcnvsn  6221  dfco2  6247  coiun  6259  co02  6263  coass  6268  ressn  6287  ovoliunlem1  25630  h2hlm  31273  cnvco1  36150  cnvco2  36151  inxprnres  38837  cnviun  44268  coiun1  44270  coxp  49496