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

Theorem iuneq12d 5020
Description: Equality deduction for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.) Remove DV conditions (Revised by GG, 1-Sep-2025.)
Hypotheses
Ref Expression
iuneq12d.1 (𝜑𝐴 = 𝐵)
iuneq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
iuneq12d (𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐷)
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)   𝐷(𝑥)

Proof of Theorem iuneq12d
Dummy variable 𝑡 is distinct from all other variables.
StepHypRef Expression
1 iuneq12d.1 . . . . . . 7 (𝜑𝐴 = 𝐵)
21eleq2d 2826 . . . . . 6 (𝜑 → (𝑥𝐴𝑥𝐵))
32anbi1d 631 . . . . 5 (𝜑 → ((𝑥𝐴𝑡𝐶) ↔ (𝑥𝐵𝑡𝐶)))
43rexbidv2 3174 . . . 4 (𝜑 → (∃𝑥𝐴 𝑡𝐶 ↔ ∃𝑥𝐵 𝑡𝐶))
54abbidv 2807 . . 3 (𝜑 → {𝑡 ∣ ∃𝑥𝐴 𝑡𝐶} = {𝑡 ∣ ∃𝑥𝐵 𝑡𝐶})
6 df-iun 4992 . . 3 𝑥𝐴 𝐶 = {𝑡 ∣ ∃𝑥𝐴 𝑡𝐶}
7 df-iun 4992 . . 3 𝑥𝐵 𝐶 = {𝑡 ∣ ∃𝑥𝐵 𝑡𝐶}
85, 6, 73eqtr4g 2801 . 2 (𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐶)
9 iuneq12d.2 . . . 4 (𝜑𝐶 = 𝐷)
109adantr 480 . . 3 ((𝜑𝑥𝐵) → 𝐶 = 𝐷)
1110iuneq2dv 5015 . 2 (𝜑 𝑥𝐵 𝐶 = 𝑥𝐵 𝐷)
128, 11eqtrd 2776 1 (𝜑 𝑥𝐴 𝐶 = 𝑥𝐵 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wcel 2107  {cab 2713  wrex 3069   ciun 4990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-v 3481  df-ss 3967  df-iun 4992
This theorem is referenced by:  disjiunb  5132  cfsmolem  10311  cfsmo  10312  wunex2  10779  wuncval2  10788  imasval  17557  lpival  21335  cnextval  24070  cnextfval  24071  dvfval  25933  fedgmullem1  33681  irngval  33736  mblfinlem2  37666  heiborlem10  37828  iunrelexpmin1  43726  iunrelexpmin2  43730  colleq12d  44277
  Copyright terms: Public domain W3C validator