Theorem eqrelriiv 5744

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ⟨cop 4591  Rel wrel 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-opab 5165  df-xp 5637  df-rel 5638

This theorem is referenced by:  eqbrriv  5745  inopab  5783  difopab  5784  inxp  5785  dfres2  6001  restidsing  6013  cnvopab  6098  cnvopabOLD  6099  cnvdif  6104  difxp  6125  cnvcnvsn  6180  dfco2  6206  coiun  6217  co02  6221  coass  6226  ressn  6246  ovoliunlem1  25436  h2hlm  30959  cnvco1  35739  cnvco2  35740  inxprnres  38273  cnviun  43632  coiun1  43634  coxp  48814