Theorem eqrelriiv 5789

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2104  ⟨cop 4633  Rel wrel 5680

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964  df-opab 5210  df-xp 5681  df-rel 5682

This theorem is referenced by:  eqbrriv  5790  inopab  5828  difopab  5829  difopabOLD  5830  dfres2  6040  restidsing  6051  cnvopab  6137  cnvdif  6142  difxp  6162  cnvcnvsn  6217  dfco2  6243  coiun  6254  co02  6258  coass  6263  ressn  6283  ovoliunlem1  25251  h2hlm  30500  cnvco1  35033  cnvco2  35034  inxprnres  37464  cnviun  42703  coiun1  42705