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

Theorem eqrelriiv 5800
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 5799 . 2 ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵)
51, 2, 4mp2an 692 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1540  wcel 2108  cop 4632  Rel wrel 5690
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 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-opab 5206  df-xp 5691  df-rel 5692
This theorem is referenced by:  eqbrriv  5801  inopab  5839  difopab  5840  difopabOLD  5841  inxp  5842  dfres2  6059  restidsing  6071  cnvopab  6157  cnvopabOLD  6158  cnvdif  6163  difxp  6184  cnvcnvsn  6239  dfco2  6265  coiun  6276  co02  6280  coass  6285  ressn  6305  ovoliunlem1  25537  h2hlm  30999  cnvco1  35759  cnvco2  35760  inxprnres  38293  cnviun  43663  coiun1  43665  coxp  48744
  Copyright terms: Public domain W3C validator