Theorem eqrelriiv 5733

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

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

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 3438  df-ss 3920  df-opab 5155  df-xp 5625  df-rel 5626

This theorem is referenced by:  eqbrriv  5734  inopab  5772  difopab  5773  inxp  5774  dfres2  5992  restidsing  6004  cnvopab  6086  cnvopabOLD  6087  cnvdif  6092  difxp  6113  cnvcnvsn  6168  dfco2  6194  coiun  6205  co02  6209  coass  6214  ressn  6233  ovoliunlem1  25401  h2hlm  30924  cnvco1  35736  cnvco2  35737  inxprnres  38270  cnviun  43627  coiun1  43629  coxp  48821