Theorem eqrelriiv 5753

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

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

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 3449  df-ss 3931  df-opab 5170  df-xp 5644  df-rel 5645

This theorem is referenced by:  eqbrriv  5754  inopab  5792  difopab  5793  difopabOLD  5794  inxp  5795  dfres2  6012  restidsing  6024  cnvopab  6110  cnvopabOLD  6111  cnvdif  6116  difxp  6137  cnvcnvsn  6192  dfco2  6218  coiun  6229  co02  6233  coass  6238  ressn  6258  ovoliunlem1  25403  h2hlm  30909  cnvco1  35746  cnvco2  35747  inxprnres  38280  cnviun  43639  coiun1  43641  coxp  48821