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

Theorem iuneq12d 4923
Description: Equality deduction for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.)
Hypotheses
Ref Expression
iuneq1d.1 (𝜑𝐴 = 𝐵)
iuneq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
iuneq12d (𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐷)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥
Allowed substitution hints:   𝐶(𝑥)   𝐷(𝑥)

Proof of Theorem iuneq12d
StepHypRef Expression
1 iuneq1d.1 . . 3 (𝜑𝐴 = 𝐵)
21iuneq1d 4922 . 2 (𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
3 iuneq12d.2 . . . 4 (𝜑𝐶 = 𝐷)
43adantr 483 . . 3 ((𝜑𝑥𝐵) → 𝐶 = 𝐷)
54iuneq2dv 4919 . 2 (𝜑 𝑥𝐵 𝐶 = 𝑥𝐵 𝐷)
62, 5eqtrd 2855 1 (𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  wcel 2114   ciun 4895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-rex 3131  df-v 3475  df-in 3920  df-ss 3930  df-iun 4897
This theorem is referenced by:  disjiunb  5031  cfsmolem  9670  cfsmo  9671  wunex2  10138  wuncval2  10147  imasval  16763  lpival  19994  cnextval  22645  cnextfval  22646  dvfval  24479  fedgmullem1  31036  mblfinlem2  34971  heiborlem10  35134  iunrelexpmin1  40188  iunrelexpmin2  40192  colleq12d  40744
  Copyright terms: Public domain W3C validator