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

Theorem ideqg 5476
Description: For sets, the identity relation is the same as equality. (Contributed by NM, 30-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
ideqg (𝐵𝑉 → (𝐴 I 𝐵𝐴 = 𝐵))

Proof of Theorem ideqg
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 22 . . 3 (𝐵𝑉𝐵𝑉)
2 reli 5452 . . . 4 Rel I
32brrelex1i 5362 . . 3 (𝐴 I 𝐵𝐴 ∈ V)
41, 3anim12ci 608 . 2 ((𝐵𝑉𝐴 I 𝐵) → (𝐴 ∈ V ∧ 𝐵𝑉))
5 eleq1 2865 . . . . 5 (𝐴 = 𝐵 → (𝐴𝑉𝐵𝑉))
65biimparc 472 . . . 4 ((𝐵𝑉𝐴 = 𝐵) → 𝐴𝑉)
76elexd 3401 . . 3 ((𝐵𝑉𝐴 = 𝐵) → 𝐴 ∈ V)
8 simpl 475 . . 3 ((𝐵𝑉𝐴 = 𝐵) → 𝐵𝑉)
97, 8jca 508 . 2 ((𝐵𝑉𝐴 = 𝐵) → (𝐴 ∈ V ∧ 𝐵𝑉))
10 eqeq1 2802 . . 3 (𝑥 = 𝐴 → (𝑥 = 𝑦𝐴 = 𝑦))
11 eqeq2 2809 . . 3 (𝑦 = 𝐵 → (𝐴 = 𝑦𝐴 = 𝐵))
12 df-id 5219 . . 3 I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
1310, 11, 12brabg 5189 . 2 ((𝐴 ∈ V ∧ 𝐵𝑉) → (𝐴 I 𝐵𝐴 = 𝐵))
144, 9, 13pm5.21nd 837 1 (𝐵𝑉 → (𝐴 I 𝐵𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385   = wceq 1653  wcel 2157  Vcvv 3384   class class class wbr 4842   I cid 5218
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-sep 4974  ax-nul 4982  ax-pr 5096
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3386  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-nul 4115  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-br 4843  df-opab 4905  df-id 5219  df-xp 5317  df-rel 5318
This theorem is referenced by:  ideq  5477  ididg  5478  poleloe  5744  isof1oidb  6801  pltval  17272  tglngne  25794  tgelrnln  25874  opeldifid  29922  ideq2  34566  idinxpss  34571  inxpssidinxp  34574  idinxpssinxp  34575  rnxrnidres  34646  cossid  34717  fourierdlem42  41098
  Copyright terms: Public domain W3C validator