Theorem fvun2 6969

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

Step	Hyp	Ref	Expression
1		uncom 4105	. . 3 ⊢ (𝐹 ∪ 𝐺) = (𝐺 ∪ 𝐹)
2	1	fveq1i 6878	. 2 ⊢ ((𝐹 ∪ 𝐺)‘𝑋) = ((𝐺 ∪ 𝐹)‘𝑋)
3		incom 4155	. . . . . 6 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
4	3	eqeq1i 2766	. . . . 5 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐵 ∩ 𝐴) = ∅)
5	4	anbi1i 636	. . . 4 ⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐵) ↔ ((𝐵 ∩ 𝐴) = ∅ ∧ 𝑋 ∈ 𝐵))
6		fvun1 6968	. . . 4 ⊢ ((𝐺 Fn 𝐵 ∧ 𝐹 Fn 𝐴 ∧ ((𝐵 ∩ 𝐴) = ∅ ∧ 𝑋 ∈ 𝐵)) → ((𝐺 ∪ 𝐹)‘𝑋) = (𝐺‘𝑋))
7	5, 6	syl3an3b 1432	. . 3 ⊢ ((𝐺 Fn 𝐵 ∧ 𝐹 Fn 𝐴 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐵)) → ((𝐺 ∪ 𝐹)‘𝑋) = (𝐺‘𝑋))
8	7	3com12 1141	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐵)) → ((𝐺 ∪ 𝐹)‘𝑋) = (𝐺‘𝑋))
9	2, 8	eqtrid 2808	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐵)) → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐺‘𝑋))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ∪ cun 3897   ∩ cin 3898  ∅c0 4279   Fn wfn 6526  ‘cfv 6531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-fv 6539

This theorem is used by:  fvun2d  6971  fveqf1o  7302  frrlem12  8299  ptunhmeo  24107  noextenddif  28007  noextendlt  28008  noextendgt  28009  noetasuplem4  28075  axlowdimlem9  29510  axlowdimlem12  29513  axlowdimlem17  29518  vtxdun  30044  isoun  33277  resf1o  33304  cycpmfvlem  33655  elrspunidl  33960  lbsdiflsp0  34240  sseqfv2  35009  actfunsnrndisj  35217  reprsuc  35227  breprexplema  35242  cvmliftlem4  36022  fullfunfv  36681  finixpnum  38496  poimirlem1  38507  poimirlem2  38508  poimirlem3  38509  poimirlem4  38510  poimirlem6  38512  poimirlem7  38513  poimirlem11  38517  poimirlem12  38518  poimirlem16  38522  poimirlem19  38525  poimirlem20  38526  poimirlem23  38529  poimirlem28  38534