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

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
StepHypRef Expression
1 eqreliiv.1 . 2 Rel 𝐴
2 eqreliiv.2 . 2 Rel 𝐵
3 eqreliiv.3 . . 3 (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)
43eqrelriv 5788 . 2 ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵)
51, 2, 4mp2an 688 1 𝐴 = 𝐵
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator