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

Theorem iuneq12d 4736
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 4735 . 2 (𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
3 iuneq12d.2 . . . 4 (𝜑𝐶 = 𝐷)
43adantr 473 . . 3 ((𝜑𝑥𝐵) → 𝐶 = 𝐷)
54iuneq2dv 4732 . 2 (𝜑 𝑥𝐵 𝐶 = 𝑥𝐵 𝐷)
62, 5eqtrd 2833 1 (𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1653  wcel 2157   ciun 4710
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-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-v 3387  df-in 3776  df-ss 3783  df-iun 4712
This theorem is referenced by:  disjiunb  4833  otiunsndisj  5176  cfsmolem  9380  cfsmo  9381  wunex2  9848  wuncval2  9857  s3iunsndisj  14050  imasval  16486  lpival  19568  cnextval  22193  cnextfval  22194  dvfval  24002  mblfinlem2  33936  heiborlem10  34106  iunrelexpmin1  38779  iunrelexpmin2  38783
  Copyright terms: Public domain W3C validator