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

Theorem eqrelriiv 5137
 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 5136 . 2 ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵)
51, 2, 4mp2an 704 1 𝐴 = 𝐵
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   = wceq 1475   ∈ wcel 1977  ⟨cop 4131  Rel wrel 5043 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-opab 4644  df-xp 5044  df-rel 5045 This theorem is referenced by:  eqbrriv  5138  inopab  5174  difopab  5175  dfres2  5372  restidsing  5377  restidsingOLD  5378  cnvopab  5452  cnv0OLD  5455  cnvdif  5458  difxp  5477  cnvcnvsn  5530  dfco2  5551  coiun  5562  co02  5566  coass  5571  ressn  5588  ovoliunlem1  23077  h2hlm  27221  cnvco1  30903  cnvco2  30904  cnviun  36961  coiun1  36963
 Copyright terms: Public domain W3C validator