ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  unieq GIF version

Theorem unieq 3715
Description: Equality theorem for class union. Exercise 15 of [TakeutiZaring] p. 18. (Contributed by NM, 10-Aug-1993.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Assertion
Ref Expression
unieq (𝐴 = 𝐵 𝐴 = 𝐵)

Proof of Theorem unieq
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rexeq 2604 . . 3 (𝐴 = 𝐵 → (∃𝑥𝐴 𝑦𝑥 ↔ ∃𝑥𝐵 𝑦𝑥))
21abbidv 2235 . 2 (𝐴 = 𝐵 → {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥} = {𝑦 ∣ ∃𝑥𝐵 𝑦𝑥})
3 dfuni2 3708 . 2 𝐴 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝑥}
4 dfuni2 3708 . 2 𝐵 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝑥}
52, 3, 43eqtr4g 2175 1 (𝐴 = 𝐵 𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316  {cab 2103  wrex 2394   cuni 3706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rex 2399  df-uni 3707
This theorem is referenced by:  unieqi  3716  unieqd  3717  uniintsnr  3777  iununir  3866  treq  4002  limeq  4269  uniex  4329  uniexg  4331  ordsucunielexmid  4416  onsucuni2  4449  nnpredcl  4506  elvvuni  4573  unielrel  5036  unixp0im  5045  iotass  5075  nnsucuniel  6359  en1bg  6662  omp1eom  6948  ctmlemr  6961  uniopn  12095  istopon  12107  eltg3  12153  tgdom  12168  cldval  12195  ntrfval  12196  clsfval  12197  neifval  12236  tgrest  12265  cnprcl2k  12302  bj-uniex  13042  bj-uniexg  13043  nnsf  13126  peano3nninf  13128  exmidsbthr  13145
  Copyright terms: Public domain W3C validator