Metamath Proof Explorer


Theorem resixp

Description: Restriction of an element of an infinite Cartesian product. (Contributed by FL, 7-Nov-2011) (Proof shortened by Mario Carneiro, 31-May-2014)

Ref Expression
Assertion resixp BAFxACFBxBC

Proof

Step Hyp Ref Expression
1 resexg FxACFBV
2 1 adantl BAFxACFBV
3 simpr BAFxACFxAC
4 elixp2 FxACFVFFnAxAFxC
5 3 4 sylib BAFxACFVFFnAxAFxC
6 5 simp2d BAFxACFFnA
7 simpl BAFxACBA
8 fnssres FFnABAFBFnB
9 6 7 8 syl2anc BAFxACFBFnB
10 5 simp3d BAFxACxAFxC
11 ssralv BAxAFxCxBFxC
12 7 10 11 sylc BAFxACxBFxC
13 fvres xBFBx=Fx
14 13 eleq1d xBFBxCFxC
15 14 ralbiia xBFBxCxBFxC
16 12 15 sylibr BAFxACxBFBxC
17 elixp2 FBxBCFBVFBFnBxBFBxC
18 2 9 16 17 syl3anbrc BAFxACFBxBC