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

Theorem eqrelriiv 5637
 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 5636 . 2 ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵)
51, 2, 4mp2an 691 1 𝐴 = 𝐵
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   = wceq 1538   ∈ wcel 2111  ⟨cop 4531  Rel wrel 5533 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877  df-opab 5099  df-xp 5534  df-rel 5535 This theorem is referenced by:  eqbrriv  5638  inopab  5676  difopab  5677  dfres2  5886  restidsing  5899  cnvopab  5974  cnvdif  5979  difxp  5998  cnvcnvsn  6053  dfco2  6080  coiun  6091  co02  6095  coass  6100  ressn  6119  ovoliunlem1  24215  h2hlm  28875  cnvco1  33254  cnvco2  33255  inxprnres  36023  cnviun  40759  coiun1  40761
 Copyright terms: Public domain W3C validator