Users' Mathboxes Mathbox for ML < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  csbfinxpg Structured version   Visualization version   Unicode version
Theorem csbfinxpg 33225
Description: Distribute proper substitution through Cartesian exponentiation. (Contributed by ML, 25-Oct-2020.)
Assertion
Ref Expression
csbfinxpg |- ( A e. V -> [_ A / x ]_ ( U ^^ ^^ N ) = ( [_ A / x ]_ U ^^ ^^ [_ A / x ]_ N ) )
Distinct variable group:   x, N
Allowed substitution hints:   A( x)   U( x)   V( x)
Proof of Theorem csbfinxpg
Dummy variables n y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-finxp 33221 . . 3 |- ( U ^^ ^^ N ) = { y | ( N e. om /\ (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) }
21csbeq2i 3993 . 2 |- [_ A / x ]_ ( U ^^ ^^ N ) = [_ A / x ]_ { y | ( N e. om /\ (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) }
3 sbcan 3478 . . . . 5 |- ( [. A / x ]. ( N e. om /\ (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) <-> ( [. A / x ]. N e. om /\ [. A / x ]. (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) )
4 sbcel1g 3987 . . . . . 6 |- ( A e. V -> ( [. A / x ]. N e. om <-> [_ A / x ]_ N e. om ) )
5 sbceq2g 3990 . . . . . . 7 |- ( A e. V -> ( [. A / x ]. (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) <-> (/) = [_ A / x ]_ ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) )
6 csbfv12 6231 . . . . . . . . 9 |- [_ A / x ]_ ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) = ( [_ A / x ]_ rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` [_ A / x ]_ N )
7 csbrdgg 33175 . . . . . . . . . . 11 |- ( A e. V -> [_ A / x ]_ rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) = rec ( [_ A / x ]_ ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , [_ A / x ]_ <. N , y >. ) )
8 csbmpt22g 33177 . . . . . . . . . . . . 13 |- ( A e. V -> [_ A / x ]_ ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) = ( n e. [_ A / x ]_ om , z e. [_ A / x ]_ _V |-> [_ A / x ]_ if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) )
9 csbconstg 3546 . . . . . . . . . . . . . 14 |- ( A e. V -> [_ A / x ]_ om = om )
10 csbconstg 3546 . . . . . . . . . . . . . 14 |- ( A e. V -> [_ A / x ]_ _V = _V )
11 csbif 4138 . . . . . . . . . . . . . . 15 |- [_ A / x ]_ if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) = if ( [. A / x ]. ( n = 1o /\ z e. U ) , [_ A / x ]_ (/) , [_ A / x ]_ if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) )
12 sbcan 3478 . . . . . . . . . . . . . . . . 17 |- ( [. A / x ]. ( n = 1o /\ z e. U ) <-> ( [. A / x ]. n = 1o /\ [. A / x ]. z e. U ) )
13 sbcg 3503 . . . . . . . . . . . . . . . . . 18 |- ( A e. V -> ( [. A / x ]. n = 1o <-> n = 1o ) )
14 sbcel12 3983 . . . . . . . . . . . . . . . . . . 19 |- ( [. A / x ]. z e. U <-> [_ A / x ]_ z e. [_ A / x ]_ U )
15 csbconstg 3546 . . . . . . . . . . . . . . . . . . . 20 |- ( A e. V -> [_ A / x ]_ z = z )
1615eleq1d 2686 . . . . . . . . . . . . . . . . . . 19 |- ( A e. V -> ( [_ A / x ]_ z e. [_ A / x ]_ U <-> z e. [_ A / x ]_ U ) )
1714, 16syl5bb 272 . . . . . . . . . . . . . . . . . 18 |- ( A e. V -> ( [. A / x ]. z e. U <-> z e. [_ A / x ]_ U ) )
1813, 17anbi12d 747 . . . . . . . . . . . . . . . . 17 |- ( A e. V -> ( ( [. A / x ]. n = 1o /\ [. A / x ]. z e. U ) <-> ( n = 1o /\ z e. [_ A / x ]_ U ) ) )
1912, 18syl5bb 272 . . . . . . . . . . . . . . . 16 |- ( A e. V -> ( [. A / x ]. ( n = 1o /\ z e. U ) <-> ( n = 1o /\ z e. [_ A / x ]_ U ) ) )
20 csbconstg 3546 . . . . . . . . . . . . . . . 16 |- ( A e. V -> [_ A / x ]_ (/) = (/) )
21 csbif 4138 . . . . . . . . . . . . . . . . 17 |- [_ A / x ]_ if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) = if ( [. A / x ]. z e. ( _V X. U ) , [_ A / x ]_ <. U. n , ( 1st ` z ) >. , [_ A / x ]_ <. n , z >. )
22 sbcel12 3983 . . . . . . . . . . . . . . . . . . 19 |- ( [. A / x ]. z e. ( _V X. U ) <-> [_ A / x ]_ z e. [_ A / x ]_ ( _V X. U ) )
23 csbxp 5200 . . . . . . . . . . . . . . . . . . . . 21 |- [_ A / x ]_ ( _V X. U ) = ( [_ A / x ]_ _V X. [_ A / x ]_ U )
2410xpeq1d 5138 . . . . . . . . . . . . . . . . . . . . 21 |- ( A e. V -> ( [_ A / x ]_ _V X. [_ A / x ]_ U ) = ( _V X. [_ A / x ]_ U ) )
2523, 24syl5eq 2668 . . . . . . . . . . . . . . . . . . . 20 |- ( A e. V -> [_ A / x ]_ ( _V X. U ) = ( _V X. [_ A / x ]_ U ) )
2615, 25eleq12d 2695 . . . . . . . . . . . . . . . . . . 19 |- ( A e. V -> ( [_ A / x ]_ z e. [_ A / x ]_ ( _V X. U ) <-> z e. ( _V X. [_ A / x ]_ U ) ) )
2722, 26syl5bb 272 . . . . . . . . . . . . . . . . . 18 |- ( A e. V -> ( [. A / x ]. z e. ( _V X. U ) <-> z e. ( _V X. [_ A / x ]_ U ) ) )
28 csbconstg 3546 . . . . . . . . . . . . . . . . . 18 |- ( A e. V -> [_ A / x ]_ <. U. n , ( 1st ` z ) >. = <. U. n , ( 1st ` z ) >. )
29 csbconstg 3546 . . . . . . . . . . . . . . . . . 18 |- ( A e. V -> [_ A / x ]_ <. n , z >. = <. n , z >. )
3027, 28, 29ifbieq12d 4113 . . . . . . . . . . . . . . . . 17 |- ( A e. V -> if ( [. A / x ]. z e. ( _V X. U ) , [_ A / x ]_ <. U. n , ( 1st ` z ) >. , [_ A / x ]_ <. n , z >. ) = if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) )
3121, 30syl5eq 2668 . . . . . . . . . . . . . . . 16 |- ( A e. V -> [_ A / x ]_ if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) = if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) )
3219, 20, 31ifbieq12d 4113 . . . . . . . . . . . . . . 15 |- ( A e. V -> if ( [. A / x ]. ( n = 1o /\ z e. U ) , [_ A / x ]_ (/) , [_ A / x ]_ if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) = if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) )
3311, 32syl5eq 2668 . . . . . . . . . . . . . 14 |- ( A e. V -> [_ A / x ]_ if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) = if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) )
349, 10, 33mpt2eq123dv 6717 . . . . . . . . . . . . 13 |- ( A e. V -> ( n e. [_ A / x ]_ om , z e. [_ A / x ]_ _V |-> [_ A / x ]_ if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) = ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) )
358, 34eqtrd 2656 . . . . . . . . . . . 12 |- ( A e. V -> [_ A / x ]_ ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) = ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) )
36 csbopg 4420 . . . . . . . . . . . . 13 |- ( A e. V -> [_ A / x ]_ <. N , y >. = <. [_ A / x ]_ N , [_ A / x ]_ y >. )
37 csbconstg 3546 . . . . . . . . . . . . . 14 |- ( A e. V -> [_ A / x ]_ y = y )
3837opeq2d 4409 . . . . . . . . . . . . 13 |- ( A e. V -> <. [_ A / x ]_ N , [_ A / x ]_ y >. = <. [_ A / x ]_ N , y >. )
3936, 38eqtrd 2656 . . . . . . . . . . . 12 |- ( A e. V -> [_ A / x ]_ <. N , y >. = <. [_ A / x ]_ N , y >. )
40 rdgeq12 7509 . . . . . . . . . . . 12 |- ( ( [_ A / x ]_ ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) = ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) /\ [_ A / x ]_ <. N , y >. = <. [_ A / x ]_ N , y >. ) -> rec ( [_ A / x ]_ ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , [_ A / x ]_ <. N , y >. ) = rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) )
4135, 39, 40syl2anc 693 . . . . . . . . . . 11 |- ( A e. V -> rec ( [_ A / x ]_ ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , [_ A / x ]_ <. N , y >. ) = rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) )
427, 41eqtrd 2656 . . . . . . . . . 10 |- ( A e. V -> [_ A / x ]_ rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) = rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) )
4342fveq1d 6193 . . . . . . . . 9 |- ( A e. V -> ( [_ A / x ]_ rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` [_ A / x ]_ N ) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) )
446, 43syl5eq 2668 . . . . . . . 8 |- ( A e. V -> [_ A / x ]_ ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) )
4544eqeq2d 2632 . . . . . . 7 |- ( A e. V -> ( (/) = [_ A / x ]_ ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) <-> (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) ) )
465, 45bitrd 268 . . . . . 6 |- ( A e. V -> ( [. A / x ]. (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) <-> (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) ) )
474, 46anbi12d 747 . . . . 5 |- ( A e. V -> ( ( [. A / x ]. N e. om /\ [. A / x ]. (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) <-> ( [_ A / x ]_ N e. om /\ (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) ) ) )
483, 47syl5bb 272 . . . 4 |- ( A e. V -> ( [. A / x ]. ( N e. om /\ (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) <-> ( [_ A / x ]_ N e. om /\ (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) ) ) )
4948abbidv 2741 . . 3 |- ( A e. V -> { y | [. A / x ]. ( N e. om /\ (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) } = { y | ( [_ A / x ]_ N e. om /\ (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) ) } )
50 csbab 4008 . . 3 |- [_ A / x ]_ { y | ( N e. om /\ (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) } = { y | [. A / x ]. ( N e. om /\ (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) }
51 df-finxp 33221 . . 3 |- ( [_ A / x ]_ U ^^ ^^ [_ A / x ]_ N ) = { y | ( [_ A / x ]_ N e. om /\ (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. [_ A / x ]_ U ) , (/) , if ( z e. ( _V X. [_ A / x ]_ U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. [_ A / x ]_ N , y >. ) ` [_ A / x ]_ N ) ) }
5249, 50, 513eqtr4g 2681 . 2 |- ( A e. V -> [_ A / x ]_ { y | ( N e. om /\ (/) = ( rec ( ( n e. om , z e. _V |-> if ( ( n = 1o /\ z e. U ) , (/) , if ( z e. ( _V X. U ) , <. U. n , ( 1st ` z ) >. , <. n , z >. ) ) ) , <. N , y >. ) ` N ) ) } = ( [_ A / x ]_ U ^^ ^^ [_ A / x ]_ N ) )
532, 52syl5eq 2668 1 |- ( A e. V -> [_ A / x ]_ ( U ^^ ^^ N ) = ( [_ A / x ]_ U ^^ ^^ [_ A / x ]_ N ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   {cab 2608   _Vcvv 3200   [.wsbc 3435   [_csb 3533   (/)c0 3915   ifcif 4086   <.cop 4183   U.cuni 4436   X. cxp 5112   ` cfv 5888   |-> cmpt2 6652   omcom 7065   1stc1st 7166   reccrdg 7505   1oc1o 7553   ^^ ^^cfinxp 33220
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-xp 5120  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-iota 5851  df-fv 5896  df-oprab 6654  df-mpt2 6655  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-finxp 33221
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator