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

Theorem fvun2 7001
Description: The value of a union when the argument is in the second domain. (Contributed by Scott Fenton, 29-Jun-2013.)
Assertion
Ref Expression
fvun2 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐵)) → ((𝐹𝐺)‘𝑋) = (𝐺𝑋))

Proof of Theorem fvun2
StepHypRef Expression
1 uncom 4158 . . 3 (𝐹𝐺) = (𝐺𝐹)
21fveq1i 6907 . 2 ((𝐹𝐺)‘𝑋) = ((𝐺𝐹)‘𝑋)
3 incom 4209 . . . . . 6 (𝐴𝐵) = (𝐵𝐴)
43eqeq1i 2742 . . . . 5 ((𝐴𝐵) = ∅ ↔ (𝐵𝐴) = ∅)
54anbi1i 624 . . . 4 (((𝐴𝐵) = ∅ ∧ 𝑋𝐵) ↔ ((𝐵𝐴) = ∅ ∧ 𝑋𝐵))
6 fvun1 7000 . . . 4 ((𝐺 Fn 𝐵𝐹 Fn 𝐴 ∧ ((𝐵𝐴) = ∅ ∧ 𝑋𝐵)) → ((𝐺𝐹)‘𝑋) = (𝐺𝑋))
75, 6syl3an3b 1407 . . 3 ((𝐺 Fn 𝐵𝐹 Fn 𝐴 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐵)) → ((𝐺𝐹)‘𝑋) = (𝐺𝑋))
873com12 1124 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐵)) → ((𝐺𝐹)‘𝑋) = (𝐺𝑋))
92, 8eqtrid 2789 1 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐵)) → ((𝐹𝐺)‘𝑋) = (𝐺𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087   = wceq 1540  wcel 2108  cun 3949  cin 3950  c0 4333   Fn wfn 6556  cfv 6561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-fv 6569
This theorem is referenced by:  fvun2d  7003  fveqf1o  7322  frrlem12  8322  ptunhmeo  23816  noextenddif  27713  noextendlt  27714  noextendgt  27715  noetasuplem4  27781  axlowdimlem9  28965  axlowdimlem12  28968  axlowdimlem17  28973  vtxdun  29499  isoun  32711  resf1o  32741  cycpmfvlem  33132  elrspunidl  33456  lbsdiflsp0  33677  sseqfv2  34396  actfunsnrndisj  34620  reprsuc  34630  breprexplema  34645  cvmliftlem4  35293  fullfunfv  35948  finixpnum  37612  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem11  37638  poimirlem12  37639  poimirlem16  37643  poimirlem19  37646  poimirlem20  37647  poimirlem23  37650  poimirlem28  37655
  Copyright terms: Public domain W3C validator