ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  xpassen Structured version   Unicode version

Theorem xpassen 6240
Description: Associative law for equinumerosity of Cartesian product. Proposition 4.22(e) of [Mendelson] p. 254. (Contributed by NM, 22-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
Hypotheses
Ref Expression
xpassen.1  _V
xpassen.2  _V
xpassen.3  C 
_V
Assertion
Ref Expression
xpassen  X.  X.  C  ~~  X.  X.  C

Proof of Theorem xpassen
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xpassen.1 . . . 4  _V
2 xpassen.2 . . . 4  _V
31, 2xpex 4396 . . 3  X. 
_V
4 xpassen.3 . . 3  C 
_V
53, 4xpex 4396 . 2  X.  X.  C 
_V
62, 4xpex 4396 . . 3  X.  C 
_V
71, 6xpex 4396 . 2  X.  X.  C 
_V
8 vex 2554 . . . . . . . . . 10 
_V
98snex 3928 . . . . . . . . 9  { }  _V
109dmex 4541 . . . . . . . 8  dom  { }  _V
1110uniex 4140 . . . . . . 7  U. dom  { }  _V
1211snex 3928 . . . . . 6  { U. dom  { } }  _V
1312dmex 4541 . . . . 5  dom  { U. dom  { } }  _V
1413uniex 4140 . . . 4  U. dom  { U. dom  { } }  _V
1512rnex 4542 . . . . . 6  ran  { U. dom  { } }  _V
1615uniex 4140 . . . . 5  U. ran  { U. dom  { } }  _V
179rnex 4542 . . . . . 6  ran  { }  _V
1817uniex 4140 . . . . 5  U. ran  { }  _V
1916, 18opex 3957 . . . 4  <. U. ran  { U. dom  { } } ,  U. ran  { } >.  _V
2014, 19opex 3957 . . 3  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.  _V
2120a1i 9 . 2  X.  X.  C  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.  _V
22 vex 2554 . . . . . . . 8 
_V
2322snex 3928 . . . . . . 7  { }  _V
2423dmex 4541 . . . . . 6  dom  { }  _V
2524uniex 4140 . . . . 5  U. dom  { }  _V
2623rnex 4542 . . . . . . . . 9  ran  { }  _V
2726uniex 4140 . . . . . . . 8  U. ran  { }  _V
2827snex 3928 . . . . . . 7  { U. ran  { } }  _V
2928dmex 4541 . . . . . 6  dom  { U. ran  { } }  _V
3029uniex 4140 . . . . 5  U. dom  { U. ran  { } }  _V
3125, 30opex 3957 . . . 4  <. U. dom  { } ,  U. dom  { U. ran  { } } >.  _V
3228rnex 4542 . . . . 5  ran  { U. ran  { } }  _V
3332uniex 4140 . . . 4  U. ran  { U. ran  { } }  _V
3431, 33opex 3957 . . 3  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.  _V
3534a1i 9 . 2  X.  X.  C  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.  _V
36 sneq 3378 . . . . . . . . . . . . . . . . 17  <. <. ,  >. ,  >.  { }  { <. <. ,  >. ,  >. }
3736dmeqd 4480 . . . . . . . . . . . . . . . 16  <. <. ,  >. ,  >.  dom  { }  dom  {
<. <. ,  >. ,  >. }
3837unieqd 3582 . . . . . . . . . . . . . . 15  <. <. ,  >. ,  >.  U. dom  { }  U.
dom  { <. <. ,  >. ,  >. }
3938sneqd 3380 . . . . . . . . . . . . . 14  <. <. ,  >. ,  >.  { U. dom  { } }  { U. dom  {
<. <. ,  >. ,  >. } }
4039dmeqd 4480 . . . . . . . . . . . . 13  <. <. ,  >. ,  >.  dom  { U. dom  { } }  dom  { U. dom  { <. <. ,  >. ,  >. } }
4140unieqd 3582 . . . . . . . . . . . 12  <. <. ,  >. ,  >.  U. dom  { U. dom  { } }  U. dom  { U. dom  { <. <. ,  >. ,  >. } }
42 vex 2554 . . . . . . . . . . . . . . . . . 18 
_V
43 vex 2554 . . . . . . . . . . . . . . . . . 18 
_V
4442, 43opex 3957 . . . . . . . . . . . . . . . . 17  <. ,  >.  _V
45 vex 2554 . . . . . . . . . . . . . . . . 17 
_V
4644, 45op1sta 4745 . . . . . . . . . . . . . . . 16  U. dom  {
<. <. ,  >. ,  >. }  <. ,  >.
4746sneqi 3379 . . . . . . . . . . . . . . 15  { U. dom  { <. <. ,  >. ,  >. } }  { <. ,  >. }
4847dmeqi 4479 . . . . . . . . . . . . . 14  dom  { U. dom  { <. <. ,  >. ,  >. } }  dom  { <. ,  >. }
4948unieqi 3581 . . . . . . . . . . . . 13  U. dom  { U. dom  { <. <. ,  >. ,  >. } }  U.
dom  { <. ,  >. }
5042, 43op1sta 4745 . . . . . . . . . . . . 13  U. dom  {
<. ,  >. }
5149, 50eqtri 2057 . . . . . . . . . . . 12  U. dom  { U. dom  { <. <. ,  >. ,  >. } }
5241, 51syl6req 2086 . . . . . . . . . . 11  <. <. ,  >. ,  >.  U. dom  { U. dom  { } }
5339rneqd 4506 . . . . . . . . . . . . . 14  <. <. ,  >. ,  >.  ran  { U. dom  { } }  ran  { U. dom  { <. <. ,  >. ,  >. } }
5453unieqd 3582 . . . . . . . . . . . . 13  <. <. ,  >. ,  >.  U. ran  { U. dom  { } }  U. ran  { U. dom  { <. <. ,  >. ,  >. } }
5547rneqi 4505 . . . . . . . . . . . . . . 15  ran  { U. dom  { <. <. ,  >. ,  >. } }  ran  { <. ,  >. }
5655unieqi 3581 . . . . . . . . . . . . . 14  U. ran  { U. dom  { <. <. ,  >. ,  >. } }  U.
ran  { <. ,  >. }
5742, 43op2nda 4748 . . . . . . . . . . . . . 14  U. ran  {
<. ,  >. }
5856, 57eqtri 2057 . . . . . . . . . . . . 13  U. ran  { U. dom  { <. <. ,  >. ,  >. } }
5954, 58syl6req 2086 . . . . . . . . . . . 12  <. <. ,  >. ,  >.  U. ran  { U. dom  { } }
6036rneqd 4506 . . . . . . . . . . . . . 14  <. <. ,  >. ,  >.  ran  { }  ran  {
<. <. ,  >. ,  >. }
6160unieqd 3582 . . . . . . . . . . . . 13  <. <. ,  >. ,  >.  U. ran  { }  U.
ran  { <. <. ,  >. ,  >. }
6244, 45op2nda 4748 . . . . . . . . . . . . 13  U. ran  {
<. <. ,  >. ,  >. }
6361, 62syl6req 2086 . . . . . . . . . . . 12  <. <. ,  >. ,  >.  U. ran  { }
6459, 63opeq12d 3548 . . . . . . . . . . 11  <. <. ,  >. ,  >.  <. ,  >.  <. U.
ran  { U. dom  { } } ,  U. ran  { } >.
6552, 64opeq12d 3548 . . . . . . . . . 10  <. <. ,  >. ,  >.  <. ,  <. , 
>. >.  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.
66 sneq 3378 . . . . . . . . . . . . . . 15  <. ,  <. ,  >. >.  { }  { <. ,  <. ,  >. >. }
6766dmeqd 4480 . . . . . . . . . . . . . 14  <. ,  <. ,  >. >.  dom  { }  dom  {
<. ,  <. ,  >. >. }
6867unieqd 3582 . . . . . . . . . . . . 13  <. ,  <. ,  >. >.  U. dom  { }  U.
dom  { <. ,  <. ,  >. >. }
6943, 45opex 3957 . . . . . . . . . . . . . 14  <. ,  >.  _V
7042, 69op1sta 4745 . . . . . . . . . . . . 13  U. dom  {
<. ,  <. ,  >. >. }
7168, 70syl6req 2086 . . . . . . . . . . . 12  <. ,  <. ,  >. >.  U. dom  { }
7266rneqd 4506 . . . . . . . . . . . . . . . . 17  <. ,  <. ,  >. >.  ran  { }  ran  {
<. ,  <. ,  >. >. }
7372unieqd 3582 . . . . . . . . . . . . . . . 16  <. ,  <. ,  >. >.  U. ran  { }  U.
ran  { <. ,  <. ,  >. >. }
7473sneqd 3380 . . . . . . . . . . . . . . 15  <. ,  <. ,  >. >.  { U. ran  { } }  { U. ran  {
<. ,  <. ,  >. >. } }
7574dmeqd 4480 . . . . . . . . . . . . . 14  <. ,  <. ,  >. >.  dom  { U. ran  { } }  dom  { U. ran  { <. ,  <. , 
>. >. } }
7675unieqd 3582 . . . . . . . . . . . . 13  <. ,  <. ,  >. >.  U. dom  { U. ran  { } }  U. dom  { U. ran  { <. ,  <. ,  >. >. } }
7742, 69op2nda 4748 . . . . . . . . . . . . . . . . 17  U. ran  {
<. ,  <. ,  >. >. }  <. ,  >.
7877sneqi 3379 . . . . . . . . . . . . . . . 16  { U. ran  { <. ,  <. ,  >. >. } }  { <. , 
>. }
7978dmeqi 4479 . . . . . . . . . . . . . . 15  dom  { U. ran  { <. ,  <. , 
>. >. } }  dom  { <. , 
>. }
8079unieqi 3581 . . . . . . . . . . . . . 14  U. dom  { U. ran  { <. ,  <. , 
>. >. } }  U.
dom  { <. , 
>. }
8143, 45op1sta 4745 . . . . . . . . . . . . . 14  U. dom  {
<. ,  >. }
8280, 81eqtri 2057 . . . . . . . . . . . . 13  U. dom  { U. ran  { <. ,  <. , 
>. >. } }
8376, 82syl6req 2086 . . . . . . . . . . . 12  <. ,  <. ,  >. >.  U. dom  { U. ran  { } }
8471, 83opeq12d 3548 . . . . . . . . . . 11  <. ,  <. ,  >. >.  <. ,  >.  <. U.
dom  { } ,  U. dom  { U. ran  { } } >.
8574rneqd 4506 . . . . . . . . . . . . 13  <. ,  <. ,  >. >.  ran  { U. ran  { } }  ran  { U. ran  { <. ,  <. , 
>. >. } }
8685unieqd 3582 . . . . . . . . . . . 12  <. ,  <. ,  >. >.  U. ran  { U. ran  { } }  U. ran  { U. ran  { <. ,  <. ,  >. >. } }
8778rneqi 4505 . . . . . . . . . . . . . 14  ran  { U. ran  { <. ,  <. , 
>. >. } }  ran  { <. , 
>. }
8887unieqi 3581 . . . . . . . . . . . . 13  U. ran  { U. ran  { <. ,  <. , 
>. >. } }  U.
ran  { <. , 
>. }
8943, 45op2nda 4748 . . . . . . . . . . . . 13  U. ran  {
<. ,  >. }
9088, 89eqtri 2057 . . . . . . . . . . . 12  U. ran  { U. ran  { <. ,  <. , 
>. >. } }
9186, 90syl6req 2086 . . . . . . . . . . 11  <. ,  <. ,  >. >.  U. ran  { U. ran  { } }
9284, 91opeq12d 3548 . . . . . . . . . 10  <. ,  <. ,  >. >.  <. <. ,  >. ,  >.  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.
9365, 92eq2tri 2096 . . . . . . . . 9  <. <. ,  >. ,  >.  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.  <. ,  <. , 
>. >.  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.
94 anass 381 . . . . . . . . 9  C  C
9593, 94anbi12i 433 . . . . . . . 8  <. <. ,  >. ,  >.  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.  C  <. , 
<. ,  >. >.  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.  C
96 an32 496 . . . . . . . 8  <. <. ,  >. ,  >.  C  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.  <. <. ,  >. ,  >.  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.  C
97 an32 496 . . . . . . . 8  <. ,  <. , 
>. >.  C  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.  <. ,  <. , 
>. >.  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.  C
9895, 96, 973bitr4i 201 . . . . . . 7  <. <. ,  >. ,  >.  C  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.  <. ,  <. , 
>. >.  C  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.
9998exbii 1493 . . . . . 6 
<. <. ,  >. ,  >.  C  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.  <. ,  <. , 
>. >.  C  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.
100 19.41v 1779 . . . . . 6 
<. <. ,  >. ,  >.  C  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.  <. <. ,  >. ,  >.  C  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.
101 19.41v 1779 . . . . . 6 
<. ,  <. ,  >. >.  C  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.  <. ,  <. , 
>. >.  C  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.
10299, 100, 1013bitr3i 199 . . . . 5 
<. <. ,  >. ,  >.  C  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.  <. ,  <. , 
>. >.  C  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.
1031022exbii 1494 . . . 4  <. <. ,  >. ,  >.  C  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.  <. ,  <. , 
>. >.  C  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.
104 19.41vv 1780 . . . 4  <. <. ,  >. ,  >.  C  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.  <. <. ,  >. ,  >.  C  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.
105 19.41vv 1780 . . . 4  <. ,  <. , 
>. >.  C  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.  <. ,  <. , 
>. >.  C  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.
106103, 104, 1053bitr3i 199 . . 3  <. <. ,  >. ,  >.  C  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.  <. ,  <. , 
>. >.  C  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.
107 elxp 4305 . . . . 5  X.  X.  C 
<. ,  >.  X.  C
108 excom 1551 . . . . 5  <. , 
>.  X.  C 
<. ,  >.  X.  C
109 elxp 4305 . . . . . . . . 9  X. 
<. ,  >.
110109anbi1i 431 . . . . . . . 8  X.  <. ,  >.  C  <. ,  >.  <. ,  >.  C
111 an12 495 . . . . . . . 8  <. ,  >.  X.  C  X.  <. ,  >.  C
112 19.41vv 1780 . . . . . . . 8  <. ,  >. 
<. ,  >.  C 
<. ,  >.  <. ,  >.  C
113110, 111, 1123bitr4i 201 . . . . . . 7  <. ,  >.  X.  C  <. ,  >.  <. ,  >.  C
1141132exbii 1494 . . . . . 6  <. , 
>.  X.  C 
<. ,  >.  <. ,  >.  C
115 exrot4 1578 . . . . . 6  <. ,  >.  <. ,  >.  C 
<. ,  >.  <. ,  >.  C
116 anass 381 . . . . . . . . 9  <. ,  >. 
<. ,  >.  C 
<. ,  >.  <. ,  >.  C
117116exbii 1493 . . . . . . . 8 
<. ,  >.  <. ,  >.  C  <. ,  >. 
<. ,  >.  C
118 opeq1 3540 . . . . . . . . . . . 12  <. ,  >.  <. , 
>.  <. <. ,  >. ,  >.
119118eqeq2d 2048 . . . . . . . . . . 11  <. ,  >. 
<. ,  >.  <. <. ,  >. ,  >.
120119anbi1d 438 . . . . . . . . . 10  <. ,  >.  <. , 
>.  C  <. <. ,  >. ,  >.  C
121120anbi2d 437 . . . . . . . . 9  <. ,  >.  <. ,  >.  C  <. <. ,  >. ,  >.  C
12244, 121ceqsexv 2587 . . . . . . . 8  <. ,  >. 
<. ,  >.  C  <. <. ,  >. ,  >.  C
123 an12 495 . . . . . . . 8 
<. <. ,  >. ,  >.  C  <. <. ,  >. ,  >.  C
124117, 122, 1233bitri 195 . . . . . . 7 
<. ,  >.  <. ,  >.  C  <. <. ,  >. ,  >.  C
1251243exbii 1495 . . . . . 6  <. ,  >.  <. ,  >.  C  <. <. ,  >. ,  >.  C
126114, 115, 1253bitri 195 . . . . 5  <. , 
>.  X.  C  <. <. ,  >. ,  >.  C
127107, 108, 1263bitri 195 . . . 4  X.  X.  C  <. <. ,  >. ,  >.  C
128127anbi1i 431 . . 3  X.  X.  C  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >. 
<. <. ,  >. ,  >.  C  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.
129 elxp 4305 . . . . 5  X.  X.  C 
<. ,  >.  X.  C
130 elxp 4305 . . . . . . . . . 10  X.  C 
<. ,  >.  C
131130anbi2i 430 . . . . . . . . 9  <. ,  >.  X.  C  <. ,  >.  <. , 
>.  C
132 anass 381 . . . . . . . . 9  <. ,  >.  X.  C  <. ,  >.  X.  C
133 19.42vv 1785 . . . . . . . . . 10  <. ,  >.  <. ,  >.  C 
<. ,  >.  <. ,  >.  C
134 an12 495 . . . . . . . . . . . 12  <. ,  >.  <. ,  >.  C  <. ,  >.  <. ,  >.  C
135 anass 381 . . . . . . . . . . . . 13  <. ,  >.  C  <. ,  >.  C
136135anbi2i 430 . . . . . . . . . . . 12  <. ,  >.  <. ,  >.  C  <. , 
>. 
<. ,  >.  C
137134, 136bitri 173 . . . . . . . . . . 11  <. ,  >.  <. ,  >.  C  <. ,  >.  <. ,  >.  C
1381372exbii 1494 . . . . . . . . . 10  <. ,  >.  <. ,  >.  C  <. ,  >.  <. ,  >.  C
139133, 138bitr3i 175 . . . . . . . . 9  <. ,  >.  <. , 
>.  C  <. ,  >.  <. ,  >.  C
140131, 132, 1393bitr3i 199 . . . . . . . 8  <. ,  >.  X.  C  <. ,  >.  <. ,  >.  C
141140exbii 1493 . . . . . . 7  <. ,  >.  X.  C 
<. ,  >.  <. ,  >.  C
142 exrot3 1577 . . . . . . 7  <. ,  >.  <. ,  >.  C  <. ,  >.  <. ,  >.  C
143 opeq2 3541 . . . . . . . . . . 11  <. , 
>.  <. ,  >.  <. ,  <. ,  >. >.
144143eqeq2d 2048 . . . . . . . . . 10  <. , 
>. 
<. ,  >.  <. ,  <. ,  >. >.
145144anbi1d 438 . . . . . . . . 9  <. , 
>.  <. ,  >.  C  <. ,  <. , 
>. >.  C
14669, 145ceqsexv 2587 . . . . . . . 8  <. ,  >.  <. ,  >.  C  <. ,  <. ,  >. >.  C
1471462exbii 1494 . . . . . . 7  <. ,  >.  <. ,  >.  C 
<. ,  <. ,  >. >.  C
148141, 142, 1473bitri 195 . . . . . 6  <. ,  >.  X.  C  <. ,  <. , 
>. >.  C
149148exbii 1493 . . . . 5  <. ,  >.  X.  C  <. ,  <. , 
>. >.  C
150129, 149bitri 173 . . . 4  X.  X.  C  <. ,  <. , 
>. >.  C
151150anbi1i 431 . . 3  X.  X.  C  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >. 
<. ,  <. ,  >. >.  C  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.
152106, 128, 1513bitr4i 201 . 2  X.  X.  C  <. U. dom  { U. dom  { } } ,  <. U. ran  { U. dom  { } } ,  U. ran  { } >. >.  X.  X.  C  <. <. U. dom  { } ,  U. dom  { U. ran  { } } >. ,  U. ran  { U. ran  { } } >.
1535, 7, 21, 35, 152en2i 6186 1  X.  X.  C  ~~  X.  X.  C
Colors of variables: wff set class
Syntax hints:   wa 97   wceq 1242  wex 1378   wcel 1390   _Vcvv 2551   {csn 3367   <.cop 3370   U.cuni 3571   class class class wbr 3755    X. cxp 4286   dom cdm 4288   ran crn 4289    ~~ cen 6155
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-en 6158
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator