MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqrelriiv Structured version   Visualization version   GIF version

Theorem eqrelriiv 5751
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
StepHypRef Expression
1 eqreliiv.1 . 2 Rel 𝐴
2 eqreliiv.2 . 2 Rel 𝐵
3 eqreliiv.3 . . 3 (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)
43eqrelriv 5750 . 2 ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵)
51, 2, 4mp2an 691 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542  wcel 2107  cop 4597  Rel wrel 5643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932  df-opab 5173  df-xp 5644  df-rel 5645
This theorem is referenced by:  eqbrriv  5752  inopab  5790  difopab  5791  difopabOLD  5792  dfres2  6000  restidsing  6011  cnvopab  6096  cnvdif  6101  difxp  6121  cnvcnvsn  6176  dfco2  6202  coiun  6213  co02  6217  coass  6222  ressn  6242  ovoliunlem1  24882  h2hlm  29964  cnvco1  34371  cnvco2  34372  inxprnres  36782  cnviun  41996  coiun1  41998
  Copyright terms: Public domain W3C validator