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

Theorem fvun2 6268
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 3755 . . 3 (𝐹𝐺) = (𝐺𝐹)
21fveq1i 6190 . 2 ((𝐹𝐺)‘𝑋) = ((𝐺𝐹)‘𝑋)
3 incom 3803 . . . . . 6 (𝐴𝐵) = (𝐵𝐴)
43eqeq1i 2626 . . . . 5 ((𝐴𝐵) = ∅ ↔ (𝐵𝐴) = ∅)
54anbi1i 731 . . . 4 (((𝐴𝐵) = ∅ ∧ 𝑋𝐵) ↔ ((𝐵𝐴) = ∅ ∧ 𝑋𝐵))
6 fvun1 6267 . . . 4 ((𝐺 Fn 𝐵𝐹 Fn 𝐴 ∧ ((𝐵𝐴) = ∅ ∧ 𝑋𝐵)) → ((𝐺𝐹)‘𝑋) = (𝐺𝑋))
75, 6syl3an3b 1363 . . 3 ((𝐺 Fn 𝐵𝐹 Fn 𝐴 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐵)) → ((𝐺𝐹)‘𝑋) = (𝐺𝑋))
873com12 1268 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐵)) → ((𝐺𝐹)‘𝑋) = (𝐺𝑋))
92, 8syl5eq 2667 1 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐵)) → ((𝐹𝐺)‘𝑋) = (𝐺𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1037   = wceq 1482  wcel 1989  cun 3570  cin 3571  c0 3913   Fn wfn 5881  cfv 5886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-sbc 3434  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-br 4652  df-opab 4711  df-id 5022  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-iota 5849  df-fun 5888  df-fn 5889  df-fv 5894
This theorem is referenced by:  fveqf1o  6554  xpsc1  16215  ptunhmeo  21605  axlowdimlem9  25824  axlowdimlem12  25827  axlowdimlem17  25832  vtxdun  26371  isoun  29464  resf1o  29490  sseqfv2  30441  actfunsnrndisj  30668  reprsuc  30678  breprexplema  30693  cvmliftlem4  31255  noextenddif  31805  noextendlt  31806  noextendgt  31807  noetalem3  31849  fullfunfv  32038  finixpnum  33374  poimirlem1  33390  poimirlem2  33391  poimirlem3  33392  poimirlem4  33393  poimirlem6  33395  poimirlem7  33396  poimirlem11  33400  poimirlem12  33401  poimirlem16  33405  poimirlem19  33408  poimirlem20  33409  poimirlem23  33412  poimirlem28  33417
  Copyright terms: Public domain W3C validator