Theorem eqbrriv 5740

Description: Inference from extensionality principle for relations. (Contributed by NM, 12-Dec-2006.)

Hypotheses

Ref	Expression
eqbrriv.1	⊢ Rel 𝐴
eqbrriv.2	⊢ Rel 𝐵
eqbrriv.3	⊢ (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)

Assertion

Ref	Expression
eqbrriv	⊢ 𝐴 = 𝐵

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

Proof of Theorem eqbrriv

Step	Hyp	Ref	Expression
1		eqbrriv.1	. 2 ⊢ Rel 𝐴
2		eqbrriv.2	. 2 ⊢ Rel 𝐵
3		eqbrriv.3	. . 3 ⊢ (𝑥𝐴𝑦 ↔ 𝑥𝐵𝑦)
4		df-br 5099	. . 3 ⊢ (𝑥𝐴𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐴)
5		df-br 5099	. . 3 ⊢ (𝑥𝐵𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	3, 4, 5	3bitr3i 301	. 2 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)
7	1, 2, 6	eqrelriiv 5739	1 ⊢ 𝐴 = 𝐵

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ⟨cop 4586   class class class wbr 5098  Rel wrel 5629

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631

This theorem is referenced by:  resco  6208  tpostpos  8188  sbthcl  9027  dfle2  13061  dflt2  13062  xpab  35920  idsset  36082  dfbigcup2  36091  imageval  36122  inxpxrn  38603  tposres0  49122